I suspect NASA chose C due to some combination of (a) the tiny verified subset they were using was secure; (b) it doesn't matter that much how secure your language is when you're spending countless sums to verify it anyway; (c) their people and/or their new hires had experience with C; (d) their systems were designed for it. None of these reasons are valid reasons to start a new, reasonably-budgeted, security-critical project in C.
Great response except for (b). The language choice matters. Some are too complex to verify in typical usage. Fortunately, despite its complexity, C was primitive enough for tools to catch up with a subset of it. One can overdo it. See INTERCAL. ;)
