3 ms·

There's a lot of interesting stuff out there about the Ariane 5 failure, whose guidance system apparently was in Ada.

johnisgood 5y ago
Not too interesting; they disabled the checks[1]. Lot of stuff have happened since then to Ada and SPARK. The Ada they used is quite different to the Ada we have today. SPARK 2014 is a complete re-design of the language, too. Plus, you are responding to a comment specifically talking about Ada/SPARK (SPARK specifically), so not sure how Ariane 5 is relevant. We already discussed it here: https://news.ycombinator.com/item?id=20931242 https://news.ycombinator.com/item?id=20931242 (and probably elsewhere, too). [1] Today those checks may not even be needed to begin with due to SPARK. GNATprove may have given them "predicate check might fail" or something like that. Read the AdaCore Blog for more.
- dandotway 5y ago
  I've used SPARK with GNAT Studio, I've used Frama-C, and I'm also experimenting with CBMC. Frama-C is way more powerful than SPARK, but also consequently has a much deeper learning curve. SPARK does not allow doubly linked lists: https://blog.adacore.com/pointer-based-data-structures-in-spark https://blog.adacore.com/pointer-based-data-structures-in-sp... For example, singly-linked lists and trees are supported whereas doubly-linked lists are not. With Frama-C you can prove doubly linked lists and all manner of complicated pointer manipulating graph algorithms. It does not impose a Rust-like pointer ownership policy as does SPARK. However, for embedded development, SPARK's restrictions are a good trade-off, as the more restrictive rules allow more proofs to be fully automated than with Frama-C and simplify diagnostic messages. A fly-by-wire avionics computer doesn't need to dynamically allocate a billion graph nodes. But SPARK is not "general purpose" like C with Frama-C is. AdaCore's SPARK tool stack is not actually written in SPARK as far as I can see, much of it is actually OCaml and Coq/Gallina for the Why3 component also used by Frama-C. See all the .ml OCaml and .v Gallina source code for yourself: https://github.com/AdaCore/why3 https://github.com/AdaCore/why3 And of course the compiler backend for Ada/SPARK is GNU GCC, written in unverified C: https://github.com/gcc-mirror/gcc/tree/master/gcc/config https://github.com/gcc-mirror/gcc/tree/master/gcc/config Compare with CompCert, the formally verified C compiler: https://github.com/AbsInt/CompCert https://github.com/AbsInt/CompCert Frama-C unfortunately requires a user to be mathematician-logician logic programming expert to fully utilize. One can begin training in Coq/Gallina with the large free online Software Foundations course: https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/

Not too interesting; they disabled the checks[1]. Lot of stuff have happened since then to Ada and SPARK. The Ada they used is quite different to the Ada we have today. SPARK 2014 is a complete re-design of the language, too. Plus, you are responding to a comment specifically talking about Ada/SPARK (SPARK specifically), so not sure how Ariane 5 is relevant. We already discussed it here: https://news.ycombinator.com/item?id=20931242 https://news.ycombinator.com/item?id=20931242 (and probably elsewhere, too). [1] Today those checks may not even be needed to begin with due to SPARK. GNATprove may have given them "predicate check might fail" or something like that. Read the AdaCore Blog for more.

dandotway 5y ago
I've used SPARK with GNAT Studio, I've used Frama-C, and I'm also experimenting with CBMC. Frama-C is way more powerful than SPARK, but also consequently has a much deeper learning curve. SPARK does not allow doubly linked lists: https://blog.adacore.com/pointer-based-data-structures-in-spark https://blog.adacore.com/pointer-based-data-structures-in-sp... For example, singly-linked lists and trees are supported whereas doubly-linked lists are not. With Frama-C you can prove doubly linked lists and all manner of complicated pointer manipulating graph algorithms. It does not impose a Rust-like pointer ownership policy as does SPARK. However, for embedded development, SPARK's restrictions are a good trade-off, as the more restrictive rules allow more proofs to be fully automated than with Frama-C and simplify diagnostic messages. A fly-by-wire avionics computer doesn't need to dynamically allocate a billion graph nodes. But SPARK is not "general purpose" like C with Frama-C is. AdaCore's SPARK tool stack is not actually written in SPARK as far as I can see, much of it is actually OCaml and Coq/Gallina for the Why3 component also used by Frama-C. See all the .ml OCaml and .v Gallina source code for yourself: https://github.com/AdaCore/why3 https://github.com/AdaCore/why3 And of course the compiler backend for Ada/SPARK is GNU GCC, written in unverified C: https://github.com/gcc-mirror/gcc/tree/master/gcc/config https://github.com/gcc-mirror/gcc/tree/master/gcc/config Compare with CompCert, the formally verified C compiler: https://github.com/AbsInt/CompCert https://github.com/AbsInt/CompCert Frama-C unfortunately requires a user to be mathematician-logician logic programming expert to fully utilize. One can begin training in Coq/Gallina with the large free online Software Foundations course: https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/