4 ms·

Yes. SPARK is a verifiable subset of Ada and can be mixed with it in the same project. There are SPARK crates you can use via Alire [1]. There's a SPARK impl

Yes. SPARK is a verifiable subset of Ada and can be mixed with it in the same project. There are SPARK crates you can use via Alire [1]. There's a SPARK implementation of the TweetNaCl crypto library[2] You can use it for general purpose programming, but it's very difficult and various degrees of verification you can achieve with it [3]. I made a verified version of Rob Pike's simple C regex matcher in SPARK -- proving an absence of runtime errors (e.g. never raise an exception or hit an out of bounds condition). [1]: https://alire.ada.dev/crates.html https://alire.ada.dev/crates.html [2]: https://github.com/rod-chapman/SPARKNaCl https://github.com/rod-chapman/SPARKNaCl [3]: https://blog.adacore.com/from-ada-to-platinum-spark-a-case-study-for-reusable-bounded-stacks https://blog.adacore.com/from-ada-to-platinum-spark-a-case-s...

hiAndrewQuinn 3y ago
Is Ada actually used outside of the US military? I'd love to hear more, I've always thought that's where it was.
- SubjectToChange 3y ago
  It’s surprisingly used a bit more in Europe than the US. You can look at AdaCore’s users/case studies to get a brief overview of industries using it.
- pjmlp 3y ago
  Yes, as mentioned on sibling comment in Europe. That is also VHDL, which is based on Ada, is also mostly used in Europe in detriment to Verilog. FOSDEM tends to have a regular Ada room. Besides military, there is avionics, transport, critical factory infrastructure, lots of stuff that falls under high integrity computing.
  - touisteur 3y ago
    We also see some people from banks passing by sometimes (critical realtime trading room apps). And medical, drones or satellites payload startups. Alas FOSDEM has changed its room attribution scheme for 'smaller' communities and IIUC there was no Ada room this year. Hopefully there'll be a space next year.
- trealira 3y ago
  In addition to what pjmlp said, it's also used by Nvidia, apparently. https://blog.adacore.com/nvidia-security-team-what-if-we-just-stopped-using-c https://blog.adacore.com/nvidia-security-team-what-if-we-jus...
pjmlp 3y ago
SPARK features have been merged into Ada 2012, so it is also available in regular code.
- touisteur 3y ago
  Ada2012 adopted the concept of design by contract, clamored by some of the biggest Ada users. At the same time of this update of the language, a large effort was in progress to modernise the 'old' spark that used contacts and proof annotations in Ada code through some kind of comment-based language. The 'merge' here was to make contracts and proof annotations actually executable Ada code (when it made sense). SPARK is first a toolsuite that examines Ada code to prove properties on this code (variable initialisation, dataflow properties, absence of runtime retors, partial or complete functional specification). The proverbe tech being only so capable, they had to restrict the supporterd language features (calling it the 'SPARK subset') for a while (most of the restrictions have been lifted in the recent year such as dynamic allocation, exceptions, aliasing) and some very hard things improved too (e.g. floating point handling). Also, to be complete, since executable contracts are not always enough, they introduced in the Ada language (for SPARK) what they call ghost code (seen and used only by the proof tools). So, yes, in a way SPARK features were merged in Ada, but you won't be able to use them for proof without the proof tools, you'll have a very expressive form of runtime assertion. Some features actually cascaded back to the compiler and the actual Ada language implementations. Also, to be easier to use for proof, the Ada2012 and 2022 language specs added a lot of sugar: quantifiers, if-expressions, case-expressions, raise-expressions, but also delta-aggregates... all greatly improving the expressivity of Ada.
bluGill 3y ago
I keep hear intriguing things about SPARK, but i'm not clear how I could try it in my projects. Part of this is I work with qt which already is different.

hiAndrewQuinn 3y ago

Is Ada actually used outside of the US military? I'd love to hear more, I've always thought that's where it was.

SubjectToChange 3y ago
It’s surprisingly used a bit more in Europe than the US. You can look at AdaCore’s users/case studies to get a brief overview of industries using it.
pjmlp 3y ago
Yes, as mentioned on sibling comment in Europe. That is also VHDL, which is based on Ada, is also mostly used in Europe in detriment to Verilog. FOSDEM tends to have a regular Ada room. Besides military, there is avionics, transport, critical factory infrastructure, lots of stuff that falls under high integrity computing.
- touisteur 3y ago
  We also see some people from banks passing by sometimes (critical realtime trading room apps). And medical, drones or satellites payload startups. Alas FOSDEM has changed its room attribution scheme for 'smaller' communities and IIUC there was no Ada room this year. Hopefully there'll be a space next year.
trealira 3y ago
In addition to what pjmlp said, it's also used by Nvidia, apparently. https://blog.adacore.com/nvidia-security-team-what-if-we-just-stopped-using-c https://blog.adacore.com/nvidia-security-team-what-if-we-jus...

pjmlp 3y ago

SPARK features have been merged into Ada 2012, so it is also available in regular code.

touisteur 3y ago
Ada2012 adopted the concept of design by contract, clamored by some of the biggest Ada users. At the same time of this update of the language, a large effort was in progress to modernise the 'old' spark that used contacts and proof annotations in Ada code through some kind of comment-based language. The 'merge' here was to make contracts and proof annotations actually executable Ada code (when it made sense). SPARK is first a toolsuite that examines Ada code to prove properties on this code (variable initialisation, dataflow properties, absence of runtime retors, partial or complete functional specification). The proverbe tech being only so capable, they had to restrict the supporterd language features (calling it the 'SPARK subset') for a while (most of the restrictions have been lifted in the recent year such as dynamic allocation, exceptions, aliasing) and some very hard things improved too (e.g. floating point handling). Also, to be complete, since executable contracts are not always enough, they introduced in the Ada language (for SPARK) what they call ghost code (seen and used only by the proof tools). So, yes, in a way SPARK features were merged in Ada, but you won't be able to use them for proof without the proof tools, you'll have a very expressive form of runtime assertion. Some features actually cascaded back to the compiler and the actual Ada language implementations. Also, to be easier to use for proof, the Ada2012 and 2022 language specs added a lot of sugar: quantifiers, if-expressions, case-expressions, raise-expressions, but also delta-aggregates... all greatly improving the expressivity of Ada.

bluGill 3y ago

I keep hear intriguing things about SPARK, but i'm not clear how I could try it in my projects. Part of this is I work with qt which already is different.