Gave #Ada #SPARK a go today. This proving stuff is quite neat, very comfortable to know that your program won't crash and that all contracts are guaranteed to be fulfilled. You of course have to make sure that you write appropriate contracts - there's no cure for stupid :)

Writeup on the blog:
http://härdin.se/blog/2018/01/20/trying-out-ada-spark/