I feel this is an interesting story to read alongside the OP: http://www.flownet.com/gat/jpl-lisp.html
I'm a big fan of functional and otherwise dynamic language, but if I had to write my own Mars-landing controller, I would use C. No doubt there.
http://www.cs.virginia.edu/~jck/publications/Xiang.Yin.disse...
C is a good choice for code generation, as a replacement for Assembler. But I would never dare write mars landing code in C directly.
I guess the curiosity team used several languages destined for a 100% verified C compiler for a well defined subset of C.
Why not? I used to write code for airborne radars directly in C, so I may have a different perspective.