Hacker News new | ask | show | jobs
by kazinator 713 days ago
If you want to prove propositions at compile time, isn't it hampering not to have Turing-complete power?
1 comments

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.