3 ms·
If people are humorously bad at reasoning about large software systems, why would they be any better at reasoning about large type systems?
by pekk 12y ago
If 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.