PML has been announced. It is "an ML like programming language, which will be extended with a prover soon."