Hacker News Reader

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.

View on HN

If you want to prove propositions at compile time, isn't it hampering not to have Turing-complete power?

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.

Reply on news.ycombinator.com