Hacker News Reader

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 turing complete language, but you can for s more restricted language.

View on HN

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/

Reply on news.ycombinator.com