You also have to worry about memory usage and runtime determinism - When restarting an engine at 10,000 feet or on takeoff[1] some things MUST happen at certain times as quickly as possible. GC isn't an option, and "oops out of memory" isn't an option either.
It comes down to it that lisp doesn't have the ecosystem behind it for life-crtical applications. I doubt it ever will.
What it is useful for though is analysis tools - helping keep people out of those life endangering situations.
Chiming in to the chorus: what do you use for that type of programming? How does it support the kinds of formal proofs you mentioned? Although I have proven the correctness of some simple code, I have found that the proof and the code can diverge too much to mean much. (Some of people interviewed in Coders at Work said the same thing.) Do your tools unify the proof and the code somehow?
Er. Doing a very quick search on Google for "real time lisp" and "embedded real time lisp" returned quite a few links and papers showing that people have and continue to be interested in such developments.
While I have personally never programed life critical stuff, I interacted closely (on the algorithmic side) with people who did. This was in the railroad industry.
They used a subset of C (no malloc...) and had a safety certified compiler. If you crash two trains because of a compiler bug at least you can pass the bunk. They did not use formal proof methods.
The documentation was massive, substantially longer than the code, to the extent that doing the actual implementation from the documentation seemed relatively trivial. Writing and analyzing the documentation on the other hand... I had the impression that writing documentation to that level of detail must have taken substantially longer than implementing it directly in code. And this was probably a good thing as it forced people to think more about every details.
Once a system was written it had to be certified. Any changes, no matter how trivial, meant you had to go through the whole certification process again: slow, painful and expensive.
Doesn't the documentation have to then become as rigorous as code --- effectively a high-level language in its own right? So writing the documentation becomes, well, just like writing a program without testing it as you go, without benefit of tests or (if desired) static type checking. If so, then the development process turns the programmer into a kind of human compiler: translating the specs into a dialect of C for the safety-certified compiler.
Actually the formal document languages have type checking and consistency analysis systems/tools.
Tools like Alloy[1] allow you to write your documentation/definition and check its consistency. These languages are always limited so you don't get into Gödel incompleteness problems.
I do avionics and am personally working slowly on an aviation startup (I hate the word!) in the experimental/homebuilt space.
Ada is used in the realtime life critical stuff because of the huge ecosystem from tools to paperwork behind it supporting safety. I could use C I suppose, but I simply am not smart enough to not miss a pointer dereference now and then.
It comes down to it that lisp doesn't have the ecosystem behind it for life-crtical applications. I doubt it ever will.
What it is useful for though is analysis tools - helping keep people out of those life endangering situations.
1. See Diamond da-42 takeoff crashes.