3 ms·
Why obsess over the compiler running into a loop? That's way less harmful than the compiled application getting into a loop on the end user's machine.
by kazinator 2y ago
Why obsess over the compiler running into a loop? That's way less harmful than the compiled application getting into a loop on the end user's machine.
- noelwelsh 2y agoI think part of the purpose of the Agda project is to see how far they can push programs as proofs, which in turn means they care a lot about termination. A language that was aimed more at industrial development would not have this restriction.
- kazinator 2y agoIf you want to prove propositions at compile time, isn't it hampering not to have Turing-complete power?
- gnulinux 2y agoNo it's not, you can write an extremely large set of programs in non-Turing complete languages. I personally consider Turing completeness a bug, not a feature, it simply means "I cannot prove the halting problem of this language" which blocks tons of useful properties. You can write useful programs in Agda. I wrote all kinds of programs in Agda including parsers and compilers.