3 ms·
Turing-completeness is difficult to avoid, and has little to do with security. For every addition to the language—browser extensions in particular—we will have
by evincarofautumn 15y ago
Turing-completeness is difficult to avoid, and has little to do with security. For every addition to the language—browser extensions in particular—we will have to very carefully prove that it cannot introduce any way to create a non-terminating function.
But in any non-trivial interactive application, termination can’t be a guarantee. The user may not ever cause the program to halt, and indeed, you want a game to run without end. Perhaps you could use a form of FRP: only the reactive part of a program would run continuously. But what would you gain?
We don’t need to make a language where programs are provably innocent. We need to make a language where assumed-guilty programs are provably imprisonable! An ordinary statically typed functional language would do just fine.
- zeteo 15y ago>Turing-completeness is difficult to avoid [...] For every addition to the language [...] we will have to very carefully prove that it cannot introduce any way to create a non-terminating function. Solving the halting problem doesn't mean all programs end - it means you can automatically determine whether an arbitrary program ends.
- evincarofautumn 15y agoYes. So? We’re not talking about the halting problem. The author wrote of total functional programming, a paradigm in which all functions and programs are provably terminating.
- zeteo 15y ago> we will have to very carefully prove that it cannot introduce any way to create a non-terminating function >The author wrote of total functional programming, a paradigm in which all functions and programs are provably terminating. So then what are you concerned about? Either use TFP, if indeed all your programs terminate, or have a different non-Turing complete approach, in which case you can still write infinite loops.