4 ms·
It is quite strange how people assume and spread the notion that types are the best or the only place to put propositions. Why ignore the option of specifying p
by mbrock 7y ago
It is quite strange how people assume and spread the notion that types are the best or the only place to put propositions. Why ignore the option of specifying propositions as separate invariants or postconditions, verified by proof, model checking, or testing? Why this focus on Curry-Howard, dependent types, and type theory?
- zozbot234 7y ago> Why ignore the option of specifying propositions as separate invariants or postconditions These are usually called 'contracts'. But there's not much of a distinction between contracts and refinement-types.
- tome 7y agoI guess it's because the idea of verifying your software in a language that's completely different from the language that you wrote it in seems uncomfortable. If your language is so good, oughtn't it be suitable for expressing its own properties?