> if I had to write my own Mars-landing controller, I would use C. No doubt there.
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.