4 ms·

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

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 4y ago
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/ 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/ada12.html http://www.ada-auth.org/standards/ada2x.html http://www.ada-auth.org/standards/ada2x.html
- touisteur 4y ago
  Also, don't hesitate to use Rosetta Code to find useful little snippets. Not all perfect but a good jump-start.
  - Jtsummers 4y ago
    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 4y ago
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'.

Jtsummers 4y ago

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/ 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/ada12.html http://www.ada-auth.org/standards/ada2x.html http://www.ada-auth.org/standards/ada2x.html

touisteur 4y ago
Also, don't hesitate to use Rosetta Code to find useful little snippets. Not all perfect but a good jump-start.
- Jtsummers 4y ago
  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 4y ago

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'.