>This is what concerns me about contract programming. With human contract law, if there's a minor typo or loophole, participants can generally see the spirit and intent, and at worst go to a judge who will usually enforce the intent. But with software contracts, only the characters matter and there's no intent anywhere: either you get paid or you don't.

It's much worse than that!! What you've just said applies to building an airplane or getting to Mars, too. Mother nature won't care what you meant to do.

But this is worse: mother nature might give you turbulence, but She won't carefully cycle or time the turbulence in a code injection vulnerability to try to get your avionics to lock up at some particular moment. With these kinds of systems, you have humans actively doing everything in their power to break the system, even using the most subtle possible tricks. It's not just noise: it's a malicious attacker.

It's not enough to "get it right". You have to get it right against someone with lockpicking tools, budget, time, and no legal, social, or moral checks and balances. By that standard, every vehicle NASA has ever built is completely broken, and NASA has never built a single thing that works.

It's not just about code that's correct. It's about code to held to literally supernatural standards of correctness.

It's a social problem.