4 ms·

I do not think that "provable" is the correct term to for the rust compiler. Type checking (safety) is only one subcategory of proofs. You can still have unprov

by mchaver 10y ago

I do not think that "provable" is the correct term to for the rust compiler. Type checking (safety) is only one subcategory of proofs. You can still have unproven behavior that will break the program at runtime that will not be prevented with a type checker. You can find higher confidence in code being correct in other programming languages. "provable" is better used to describe interactive (Coq, Isabelle, etc.) and automatic (Z3) theorem proving languages. Interactive theorem provers generally require a large amount of work on the coders part. Automatic theorem provers are limited in the types of problems they can prove. I am sure they can still run into runtime issues.

adrianratnapala 10y ago
I did not mean that the Rust compiler proves your code is correct. Or that it proves more than any other compiler. But like all type-checkers, it does prove that your code obeys certain rules. In a trivial way this is even true of C -- but languages like Rust and Ada go further and prove that you are avoiding large classes of common bugs.
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 ago
  You'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.

by mchaver 10y ago

adrianratnapala 10y ago

I did not mean that the Rust compiler proves your code is correct. Or that it proves more than any other compiler. But like all type-checkers, it does prove that your code obeys certain rules. In a trivial way this is even true of C -- but languages like Rust and Ada go further and prove that you are avoiding large classes of common bugs.

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 ago
You'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.