I learned a great tool, Why3 in May with Jean-Christophe Filliatre.

I am going to post the few lab exercises here. it is really fun.

It is little different coding because it is based on formal methods and proofs.

But I think you will get this fast.

The Why3 GUI is launched with the following command: why3 ide file.mlw


Why3 standard library