> The level of complexity that shows up in these system scares me. Even when introducing languages like Ada, people find a way to abuse them. Budgets get tight, schedules slip, and verification gets lax.

That is the absolute major issue with doing safety-critical development right: it has a cost, that cost is very, very high, and few want to pay it.

One of the few groups I'm aware of which does pay it is the (now defunct, I guess) software shuttle group. Their work was expensive, it was process-heavy (the 1997 story on them quoted 2500 pages of spec for GPS integration which ended up totaling 6.3kloc change to the source, 1.5% of it) but they delivered exactly what they were set to: critically safe code (in fact, if I remember correctly the Shuttle software group is the only area of NASA Feynman praised in his Challenger report)