Foundational Cryptography in SPARK

Very impressive work! I always wondered in which way contract programming will move. This is one aspect where I see the human factor never being really phased out, because you need people to check the contracts. Ada/SPARK are languages that are just very nice to work with.

I would like to encourage everyone to play around with them!