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.

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.

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.

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

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

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

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

Compare with CompCert, the formally verified C compiler:

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/