3 ms·
SDV proves properties that are in general undecidable, and as such it is not possible to substitute the Rust type checker for it. The critical difference is tha
by ulber 10y ago
SDV proves properties that are in general undecidable, and as such it is not possible to substitute the Rust type checker for it. The critical difference is that software verification algorithms are allowed to be partial (i.e. not terminate or return "unknown"), while type checking algorithms are required to be total.
Edit: Another way to look at it is that software verification tools find proofs for properties, while type checkers only verify proofs (given as the program structure and type annotations).
- geon 10y agoBut couldn't the type system guarantee a sufficent subset of all the possible interactions with the api? Like, you can't determine the halting problem for a turing complete language, but you can for s more restricted language.
- ulber 10y agoOne option which allows you to keep Turing completeness is just asking the user to write more annotations, such as loop invariants and termination conditions. For example the Dafny [1] language+verifier does this: it automates the tedious parts of the proofs but requires the user to give the hard parts (loop invariants) as annotations. [1]: http://research.microsoft.com/en-us/projects/dafny/ http://research.microsoft.com/en-us/projects/dafny/