4 ms·
>Why this effort to make a language in which many programs can’t be written? Because TC is intimately tied to Godel’s incompleteness theorems & Rice’s theorem,
by crdoconnor 11y ago
>Why this effort to make a language in which many programs can’t be written? Because TC is intimately tied to Godel’s incompleteness theorems & Rice’s theorem, allowing TC means that one is forfeiting all sorts of provability properties: in a non-TC language, one may be able to easily prove all sorts of useful things to know; for example, that programs terminate
Non-turing complete languages are also easier to reason about, less susceptible to bugs and less susceptible to technical debt.
For this reason minimizing as much as possible the amount of turing complete code you write will make your code cleaner.
Configuration and tests in particular are usually best described in a non-turing complete language.
- marcosdumay 11y ago>Non-turing complete languages are also ... less susceptible to technical debt. Well, except the technical debt of writing all the code in a language that may not support solving your problem once you know it better.
- crdoconnor 11y agoIf it doesn't actually solve the problem you have a non-functional program, not technical debt.
- Moshe_Silnorin 11y agoYou have a non-functional total functional program.
- bbrazil 11y agoAt least in terms of configuration management, what you usually end up with have is a complex config generated by something that is Turing complete. Better to start out and keep the core configuration representation simple (e.g. json, protobuf, ini file) and generated by something powerful like Flabbergast.org.
- marcosdumay 11y ago"Technical default" may be a better name for it.
- Kutta 11y agoTechnically speaking, for each program in a TC language we can have a program in a coinductive total language with the same observable behavior. In nutshell to those who may not be familiar with the field: total languages differ from partial TC languages in that they must always include internally a "hit the reset button" exit from potential infinite loops, and this is enforced by the type system. Since we can't actually observe an infinite number of program steps even in TC languages, this makes total languages effectively just as powerful as TC ones, but total languages are better-behaved in the sense that we can make a statically enforced distinction between provably terminating and possibly nonterminating code, therefore having all optimization/reasoning benefits in total parts, but also infinite processes in coindutive parts.
- marcosdumay 11y agoWell, I shrug to think about how people would create a program that runs for an indeterminate time (that's most useful ones) in a coinductive total language. Yes, in practice it must be possible. Then, total languages are just a subset of the non TC languages, and those are as prone to accumulating technical debit as TC languages. For avoiding technical debit, one needs something much less expressive.
- mietek 11y agoKudos. I wish this point of view was as commonly accepted as you present it.
- lmm 11y ago> Non-turing complete languages are also easier to reason about, less susceptible to bugs and less susceptible to technical debt. Citation needed. Not my experience at all. Some well-designed total functional languages perhaps, but not non-turing complete languages in general, and not the typical alternatives for configuration and tests.
- crdoconnor 11y agoHave you tried ansible?
- lmm 11y agoYes, but I don't see the relevance. Ansible is turing-complete, as are all the alternatives in that space AFAIK.
- crdoconnor 11y agoTechnically states are turing complete because of the command module but in practice it's as if it weren't. It's a hell of a lot cleaner than other DSLs, especially puppet's ruby-turing-complete one.
- lmm 11y agoShrug. Not my experience of it in practice.