3 ms·
No, dependent types are no the answer - read (or watch) this: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-a
by mkleczek 4y ago
No, dependent types are no the answer - read (or watch) this: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity
- miloignis 4y agoI have in the past, and I belive that they are either mistaken or they are claiming something uncontroversial that is misunderstood. In any case, you don't need dependent types for a compiler to prove termination, it's just that most languages don't care about termination except those with dependent types. You could create a compiler for Rust that has similar termination checking to Coq, if you wanted.
- mkleczek 4y agoAhh, I misread your comment. Indeed, halting is not very interesting property of programs.
- deterministic 4y agoCompCert disagrees.