4 ms·

If it's so tedious, maybe someone can come up with a more unified language that accomplishes the same thing?

dandotway 5y ago
And if cancer kills millions every year and successful treatments are expensive and tedious, maybe someone can come up with a cure to cancer that is not expensive and not tedious. It's a hard problem to solve, but a lot of smart people are working on that problem, too.
- perl4ever 5y ago
  Solving cancer is a fundamentally new thing that nobody knows how to do yet and probably can't be done by one person. Taking an ugly language that evolved in parts and synthesizing it into something elegant is something that not everybody can do, but it only takes one talented person, and it's been done before. Craft rather than invention.
johnisgood 5y ago
We have Ada/SPARK already. SPARK is a subset of Ada that allows you to formally verify your code, e.g. to prove the absence of runtime errors, memory leaks, and so forth.
- perl4ever 5y ago
  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/

And if cancer kills millions every year and successful treatments are expensive and tedious, maybe someone can come up with a cure to cancer that is not expensive and not tedious. It's a hard problem to solve, but a lot of smart people are working on that problem, too.

perl4ever 5y ago
Solving cancer is a fundamentally new thing that nobody knows how to do yet and probably can't be done by one person. Taking an ugly language that evolved in parts and synthesizing it into something elegant is something that not everybody can do, but it only takes one talented person, and it's been done before. Craft rather than invention.

johnisgood 5y ago

We have Ada/SPARK already. SPARK is a subset of Ada that allows you to formally verify your code, e.g. to prove the absence of runtime errors, memory leaks, and so forth.

perl4ever 5y ago
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/