4 ms·

I love this paper. The idea of non-Turing-complete languages that are quite useful for real work (whatever that means) is such a fascinating concept. Knowing at

I love this paper. The idea of non-Turing-complete languages that are quite useful for real work (whatever that means) is such a fascinating concept. Knowing at compile time that my program won't run off in unending or unproductive code seems like such a useful bit of static checking. There are also essentially no total languages today. Idris, Coq, etc. have support for totality, but there's nothing widespread or simple that does. I expect a total language would be quite useful in certain contexts (real-time, scripting, running user code, compilers), but the drive for - I can do whatever I want in this language - is so strong that a total language would need to provide significant, useful advantages to see adoption.

JadeNB 10y ago
> There are also essentially no total languages today. As you obviously meant, no total general-purpose languages. I'm sure that HTML is total, for example. You also later qualified that "no total languages" meant "no widespread, simple, total languages", which I think is a very different statement!
- oconnor0 10y ago
  Yes, there's also the subset of SQL that is total - or, at least, not-Turing-complete. Edit: As far as HTML goes, I was attempting to describe "programming languages" - or perhaps algorithmic languages - which I don't consider HTML falling under.
  - lgas 10y ago
    Is that not true of every not-total/turing-complete language?
- gue5t 10y ago
  HTML has no reduction/evaluation rules and so it can't have a semantics in the same way as real programming languages. You could think of a "layout semantics" relating HTML and a given environment (screen size, fonts, etc.) to the resulting box model or rendered page, but that's not very interesting from the standpoint of totality: we already know that Web browsers are supposed to show something no matter how mangled their input is.
  - JadeNB 10y ago
    > HTML has no reduction/evaluation rules and so it can't have a semantics in the same way as real programming languages. It seems to me that your next sentence addresses this better than I could. > that's not very interesting from the standpoint of totality: we already know that Web browsers are supposed to show something no matter how mangled their input is. So isn't it interesting that they do that? I think that the prevalence of scripting languages on the modern web (and, if you like to look farther back in history, the reluctant Turing completeness of TeX) strongly suggests that it wasn't at all inevitable that we would get a total language for web design. That is, to prove that it is total is presumably not much of an accomplishment, but that it is total is very interesting (and, from the point of view of the success of the web, important) indeed.
anonymousDan 10y ago
Datalog?
chriswarbo 10y ago
Regular expressions are widely used, and they're written in a total language (at least, originally; PCREs are certainly not regular, although I don't recall seeing proof that they're universal).
pron 10y ago
There are two problems: 1. Totality doesn't guarantee that your program would actually terminate. A program that loops 2^100 times never terminates, yet is provably total. It is possible that empirically programs that are proven total turn out more likely to terminate, but in that case there is no need to enforce totality everywhere. You can prove termination whenever you like. 2. Proving totality can be extremely hard (yet another reason not to enforce it everywhere). So much so that Xavier Leroy, the world-expert who wrote CompCert, the only real-world, non-trivial program ever written in Coq, found termination proofs so difficult that he skipped them in CompCert, instead inserting a counter that he thought would suffice and throwing a runtime exception if it ever runs out before the function terminates. As to total programming languages, safety-critical real-time software sometimes makes use of languages that are finite-state-machines, a far more restrictive model than Turner's total language. Nevertheless, bear in mind that even for FSMs, program verification is not generally tractable. How easy it is to verify a program depends almost entirely on one thing: how simple your algorithm is. All sorts of linguistic restrictions or safe runtimes can help prevent very important classes of bugs (like memory safety) that are local program properties, but do very little to make the cost of more global, logical properties affordable (which isn't surprising given that even the most restrictive computation model, the FSM, doesn't yield generally feasible verification).

JadeNB 10y ago

> There are also essentially no total languages today. As you obviously meant, no total general-purpose languages. I'm sure that HTML is total, for example. You also later qualified that "no total languages" meant "no widespread, simple, total languages", which I think is a very different statement!

oconnor0 10y ago
Yes, there's also the subset of SQL that is total - or, at least, not-Turing-complete. Edit: As far as HTML goes, I was attempting to describe "programming languages" - or perhaps algorithmic languages - which I don't consider HTML falling under.
- lgas 10y ago
  Is that not true of every not-total/turing-complete language?
gue5t 10y ago
HTML has no reduction/evaluation rules and so it can't have a semantics in the same way as real programming languages. You could think of a "layout semantics" relating HTML and a given environment (screen size, fonts, etc.) to the resulting box model or rendered page, but that's not very interesting from the standpoint of totality: we already know that Web browsers are supposed to show something no matter how mangled their input is.
- JadeNB 10y ago
  > HTML has no reduction/evaluation rules and so it can't have a semantics in the same way as real programming languages. It seems to me that your next sentence addresses this better than I could. > that's not very interesting from the standpoint of totality: we already know that Web browsers are supposed to show something no matter how mangled their input is. So isn't it interesting that they do that? I think that the prevalence of scripting languages on the modern web (and, if you like to look farther back in history, the reluctant Turing completeness of TeX) strongly suggests that it wasn't at all inevitable that we would get a total language for web design. That is, to prove that it is total is presumably not much of an accomplishment, but that it is total is very interesting (and, from the point of view of the success of the web, important) indeed.

anonymousDan 10y ago

Datalog?

chriswarbo 10y ago

Regular expressions are widely used, and they're written in a total language (at least, originally; PCREs are certainly not regular, although I don't recall seeing proof that they're universal).

pron 10y ago

There are two problems: 1. Totality doesn't guarantee that your program would actually terminate. A program that loops 2^100 times never terminates, yet is provably total. It is possible that empirically programs that are proven total turn out more likely to terminate, but in that case there is no need to enforce totality everywhere. You can prove termination whenever you like. 2. Proving totality can be extremely hard (yet another reason not to enforce it everywhere). So much so that Xavier Leroy, the world-expert who wrote CompCert, the only real-world, non-trivial program ever written in Coq, found termination proofs so difficult that he skipped them in CompCert, instead inserting a counter that he thought would suffice and throwing a runtime exception if it ever runs out before the function terminates. As to total programming languages, safety-critical real-time software sometimes makes use of languages that are finite-state-machines, a far more restrictive model than Turner's total language. Nevertheless, bear in mind that even for FSMs, program verification is not generally tractable. How easy it is to verify a program depends almost entirely on one thing: how simple your algorithm is. All sorts of linguistic restrictions or safe runtimes can help prevent very important classes of bugs (like memory safety) that are local program properties, but do very little to make the cost of more global, logical properties affordable (which isn't surprising given that even the most restrictive computation model, the FSM, doesn't yield generally feasible verification).