4 ms·
Humans are humorously bad at reasoning about large software systems written by a large number of people. Even if all the code you personally write is locally sa
by freyrs3 12y ago
Humans are humorously bad at reasoning about large software systems written by a large number of people. Even if all the code you personally write is locally safe, it's very very difficult to guarantee that the interaction of it with all other components written by other people is itself safe.
That's why formal methods ( type systems, model checkers, ... ) are extremely important, the only to reason about programs in the large is to prove properties of the system that are machine-checkable and remove the need for manual proofs that admit error.
- pekk 12y agoIf people are humorously bad at reasoning about large software systems, why would they be any better at reasoning about large type systems?
- freyrs3 12y agoBecause type systems, at least in the ML tradition, reduce down to systems of logic that we already know how to prove properties about. We can prove progress and preservation of a type system, and we even have systems to mechanically check those proofs.