Most high-reliability software is still written in C or other languages in the algol family. For the highest level of assurances, often the binary code must be mapped back to the source code (to reduce the chances of a compiler bug introducing errors), and doing so in languages that are higher-level than C becomes problematic.

If someone were to formally verify the correctness of a particular higher-level language implementation, then it would start to become usable. Most GCed languages are out though due to the fact that hard-realtime GC algorithms require an excess of CPU and RAM to run correctly, and vehicles going into space are often several generations of hardware behind, as new radiation-hardened CPUs come out only rarely.

NASA did use Lisp in the past.

Super nit-pick but if you are talking about the DS1, I believe it was JPL under contract for NASA.