3 ms·

But 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 tu

• ulber 11y ago
  One 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/