Hacker News new | ask | show | jobs
by kazinator 712 days 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.
1 comments
noelwelsh 711 days ago
I 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.
link
kazinator 711 days ago
If you want to prove propositions at compile time, isn't it hampering not to have Turing-complete power?
link
gnulinux 706 days ago
No 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.

link