[eatonphil]

This is a fantastic post! It's great to have a concrete example of proving a not-trivial algorithm. And somehow this Ada code feels more approachable to me than HOL4 and other functional proof assistants I've looked at.

While it's been on my list for a while, I'm more curious to try out Ada now.

[Jtsummers]

It'll take you less than a week to get proficient enough in it to make something useful, or at least interesting. It's a very straightforward language, overall.

https://learn.adacore.com/ - Pretty much the best free source until you're actually ready to commit to the language. The "Introduction to Ada" course took me maybe a week of 1-2 hours a day reading and practicing to go through. There's also a SPARK course that takes a bit longer, but is also interactive.

The language reference manuals for 2012 and 202x (which should become Ada 2022):

http://www.ada-auth.org/standards/ada12.html

http://www.ada-auth.org/standards/ada2x.html

[touisteur]

Also, don't hesitate to use Rosetta Code to find useful little snippets. Not all perfect but a good jump-start.

[Jtsummers]

Yep, I wrote a bunch of those RC examples too. It was a useful exercise when I decided to learn Ada (and with other languages, too).

[touisteur]

Two of the most interesting things that trickled down during the design of Spark2014:

1- contracts are written in the same language as the code to be checked/proved. This made important to add expressive features to the language (for all / for some: quantifiers! expression functions, if- and case-statements and more recently the new delta-aggregates notation): these additions make the language far more expressive without too much loss of readability.

2- executable contracts: most contracts can be checked at runtime or proved. And the escape hatch (code only present for proof) is 'ghost' code which is also a nice addition.

Lots of little nifty additions to the language, from just 'thinking in contracts' or 'designing for probability'.