Re:Checked C
by GoblinSlayer on Thursday December 22, 2022 @03:54AM
(#34091230)
It's justified for aerospace, because failures are quite expensive there, but for usual business it will be much easier to implement automatic bound checking, like at 1% complexity of the C compiler.
I wonder what operating systems the aerospace industry uses, since failures in the operating system could be equally expensive, yet operating system developers generally do not have access to these tools.
This is not entirely true. Patrick Cousot‘s group, which invented the theory of abstract interpretation, kept working on it and produced Astree.
I had previously been under the impression that Astree was from the same people that made Compcert C, but upon double checking for this reply, I realized that was wrong. The two groups are both in France though. It was an easy mistake to make considering that Absint sells licenses for both.
> Trying to make static guaranties about imperative code is indeed a dead end by now.
The astree static analyzer is available from Absint. One of the inventors of both it and the theory on which it is based is also still alive:
https://en.wikipedia.org/wiki/Patrick_Cousot
His software is in use at the ESA and other places.
NASA is using software it wrote in house based on that theory:
https://www.nasa.gov/aero/ikos.html
Presumably, NASA heard about Astree from the ESA and decided to make its own tool, possibly due to NIH syndrome. I am not sure if NASA counts as academia.
This is far from a dead end, even if most researchers cannot be bothered to do things in that area. You will probably find a number of the ones that can be bothered to do things in that area at farma-c:
https://frama-c.com/