4 ms·

The halting problem is not a big deal in practice. Plenty of compilers for many programming/proof languages out there (Agda, Idris, Coq, LEAN etc.) will reject

The halting problem is not a big deal in practice. Plenty of compilers for many programming/proof languages out there (Agda, Idris, Coq, LEAN etc.) will reject code that the compiler can’t prove is terminating. And yet those programming languages are more than powerful enough for writing real world software. Including operating systems, compilers etc. A good introduction to this subject is the book “Type Driven Development in Idris” or one of the Agda books.

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 ago
  I 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 ago
    Ahh, I misread your comment. Indeed, halting is not very interesting property of programs.
- deterministic 4y ago
  CompCert disagrees.