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