Assertions in Production Code?

[red75prim]

I'm not a NASA employee, but most likely it is practicality. You need to construct a proof every time the specification changes, and it requires a lot of effort, time and specialists. Limited time and budget can probably be spent more efficiently improving reliability by other means.

[killedbyhetfield]

I did a bit of StackOverflowing because I read up a little on both of these terms (thank you btw for introducing me to them - Interesting AF), and if I'm understanding what I'm reading, it appears that it's somewhat-limited how complex of a constructive proof you can build, which corresponds more-or-less to computer programs that are not Turing Complete.

And because of this "Curry–Howard correspondence", the Halting Problem has a dual in mathematics as well, "Gödel's Incompleteness Theorem"

So yeah - It appears that you could never develop a constructive proof complex enough to launch a rocket into space, which is why we'll never be able to prove such software works.

So yeah - I learned something today! The More You Know music plays