> Academia decided that this isn't realistically "feasible" and moved on to some much simpler approaches like pure functional programming and prove systems base

> Academia decided that this isn't realistically "feasible" and moved on to some much simpler approaches like pure functional programming and prove systems bases on depended types. 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 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 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/ https://frama-c.com/