5 ms·

My personal conclusion is a need for "escape hatches" in any language with strong constraints rather than an indictment of Turin-incompleteness in general. The

My personal conclusion is a need for "escape hatches" in any language with strong constraints rather than an indictment of Turin-incompleteness in general. The usual criticism that is leveled at Turing-incomplete languages is "well you've only changed the problem from taking an infinite time to taking more time than the heat death of the universe which really isn't that much better," but that's completely ignoring the ergonomics of how this actually plays out in real-life coding. In real-life coding, the choice is almost never between "does not terminate" and "heat death of the universe." When we write buggy, non-terminating code, the fix is usually a small change that takes it from "does not terminate" to "terminates in a reasonable amount of time." The fix usually does not take it to "indistinguishable from non-termination." This might be forgetting a base case in a recursive definition or getting a loop termination condition wrong. More insidiously this can happen when termination conditions are based off of non-local things and therefore depend on assumptions that "far away" from the original code. The point of Turing-incomplete languages is to go after those use cases, where the function would otherwise complete in a reasonable amount of time, save for one small little issue. What the article is pointing out is that in pursuit of that dream, the language can be overly restrictive to the point that people are forced to write "heat death"-style functions to get around its restrictions. This is an important distinction! People aren't accidentally writing functions that take insane amounts of time to complete in Turing-incomplete languages, but are rather doing so intentionally because that's the only way they can get their desired functionality. This is why the analogy of "non-termination" to "termination after the heat death of the universe" doesn't work. The former occurs when people don't realize that they've done that. The latter is a conscious, angry choice by users. That's why I think you need escape hatches to make sure people aren't forced to abuse the language when its restrictions really make a certain task impossible to complete in a reasonable amount of time.

nextos 6y ago
I think it's not just about termination, it's broadly about restricted semantics. If we had a meta-language like Lisp or ML that had very good capabilities to quickly develop DSLs with very clean restricted semantics for every particular component of a big system, and tooling to automate proofs for said restricted semantics, it'd be much easier to prove the validity of any piece of code. The scenario we currently have is quite different, so it requires heroic efforts to get any kind of guarantee on big systems (e.g. the Astree static analyzer or seL4). Citing Alan Perlis: "Beware of the Turing tar pit, where everything is possible but nothing of interest is easy".
- rstuart4133 6y ago
  > Citing Alan Perlis: "Beware of the Turing tar pit, where everything is possible but nothing of interest is easy". I posited here on HN Postscript / PDF recently is just such a tar pit, but got down voted for it. If you've every tried to copy and paste from a PDF and got rubbish (as opposed to a message saying you aren't allowed to do that), the reason is the Turning complete program painting the page doesn't have to paint things in a particular order and the things it paints may be bit maps. In the worst case you may as well be trying to copy a bunch of PNG images that have been plonked onto the canvas that happen to look like letters to a human. We would have been far better off with a declarative way of painting a page. It's not that hard - SVG achieves the same end result, and is purely declarative.

nextos 6y ago

I think it's not just about termination, it's broadly about restricted semantics. If we had a meta-language like Lisp or ML that had very good capabilities to quickly develop DSLs with very clean restricted semantics for every particular component of a big system, and tooling to automate proofs for said restricted semantics, it'd be much easier to prove the validity of any piece of code. The scenario we currently have is quite different, so it requires heroic efforts to get any kind of guarantee on big systems (e.g. the Astree static analyzer or seL4). Citing Alan Perlis: "Beware of the Turing tar pit, where everything is possible but nothing of interest is easy".

rstuart4133 6y ago
> Citing Alan Perlis: "Beware of the Turing tar pit, where everything is possible but nothing of interest is easy". I posited here on HN Postscript / PDF recently is just such a tar pit, but got down voted for it. If you've every tried to copy and paste from a PDF and got rubbish (as opposed to a message saying you aren't allowed to do that), the reason is the Turning complete program painting the page doesn't have to paint things in a particular order and the things it paints may be bit maps. In the worst case you may as well be trying to copy a bunch of PNG images that have been plonked onto the canvas that happen to look like letters to a human. We would have been far better off with a declarative way of painting a page. It's not that hard - SVG achieves the same end result, and is purely declarative.