3 ms·
> I do not think that "provable" is the correct term to for the rust compiler. If it was, in every sense, the right term, there would be a lot more fuss around
by posterboy 10y ago
> I do not think that "provable" is the correct term to for the rust compiler.
If it was, in every sense, the right term, there would be a lot more fuss around that.
> Type checking (safety) is only one subcategory of proofs
I hardly know what I'm speaking of, but these lemmas on nLab [1,2] seem to imply more than that.
[1] https://ncatlab.org/nlab/show/propositions+as+types https://ncatlab.org/nlab/show/propositions+as+types
[2] https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory https://ncatlab.org/nlab/show/relation+between+type+theory+a...
- mchaver 10y agoYou're right, I should amend this statement: > Type checking (safety) is only one subcategory of proofs Type checking as provided by Rust, Haskell, etc. only covers a subset of possible proofs. Liquid Haskell goes further to increase the range of possible proofs it covers through type checking by using automatic theorem provers.