Hacker News Reader

What does provably correct mean here? I think you mean that the code doesn’t have any memory corruption vulnerabilities. However, that is only one class of vulnerability, so more techniques then just relying on a memory safe language are required for secure software.

View on HN

It means that the type system can prove certain properties for you. For example, in languages with dependent type systems like Agda, you can construct a sorted list type that the compiler will prove it sorted at all times, otherwise it won’t compile. Or a complex tree type that is always balanced. Or a set of only even numbers, and again it won’t compile otherwise…

(Sadly, if you go that far, it isn’t generally Turing complete anymore. Though in some cases that’s a good thing.)

Reply on news.ycombinator.com