Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

I just wish more people understood that something being Turing Complete isn't a feature, it's a flaw.


Turing completeness may be a flaw, but it is nearly impossible to avoid.


Not true at all. It is hard, but not impossible. Technologically it's very challenging because we don't have non-TC programming languages that are able to keep up with modern ones. But, for example, we have (safe) Agda which is not TC (all programs marked --safe should prove to halt) and you can write useful programs. Here, "useful" is a subjective qualifier, but I personally implemented many parsers in Agda (including a json parser) so for my definition of useful, Agda is one such language.


I didn't say it was impossible. I said it was nearly impossible, which is a synonym for "hard" for some value of hard.

Case in point: I looked into Agda and ended up in a deep rabbit hole that involved something I had never heard of called "Walther recursion." Whether this qualifies as "nearly impossible" or merely "hard" is quibbling over terminology, not substance.


I've been writing programs in Agda for years (since when they didn't have sized types or cubical theory) but I never heard "Walther recursion" before. If this is your day 0 I doubt you need to know about it to understand the language.


Corresponding paper is probably http://people.csail.mit.edu/kostas/papers/CADE1996.pdf. Thanks for the name drop, looks great


How so?


E.g. you can require all programs to halt, which makes the language non-TC since the language has a trivial solution to its halting problem. There are other ways too, but this is approach e.g. Agda takes.

Note that you can still build useful programs this way since such languages can still allow certain forms of recursion such as primitive recursion, structural recursion etc... You can also use sized types [1] to allow even a larger set of (halting) programs.

[1] This is a way of compiler statically analyzing the size of each type (i.e. how many recursive constructors necessary) which puts an upper bound on the number of recursions need to be performed.


If your type system or log formatter is turing-complete, it can be exploited to do arbitrary unintended things.


Also, Turing Completeness is almost always accidental while non-TC is obtained by design. Hence, just about anything has Turing Completness which doesn't make it a feature.

Now if you want to gain the ability to make serious proofs about your programs, one can make the argument you need non-TC.


Maybe the previous speaker means the "tragedy of Common Lisp", where (in my understanding of the problem) it was happened to became too much of clever developers which decided to add too much of clever things in main library which are required to be known for keep writing the compiler in same code style (I am not a real programmer but have a sympathy to that answer, please correct me for creating more precise answer).




Consider applying for YC's Winter 2026 batch! Applications are open till Nov 10

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: