4 ms·

It's pretty hard to make something that is not turing-complete. I've always wondered if it wouldn't be beneficial to have a turing-incomplete language given tha

It's pretty hard to make something that is not turing-complete. I've always wondered if it wouldn't be beneficial to have a turing-incomplete language given that Rice's theorem then doesn't necessarily hold and thus very powerful semantic analysis might be possible. But the language is then probably not practical due to limited expressiveness.

gpderetta 6y ago
Total Functional Programming is a thing [1]. [1] https://en.wikipedia.org/wiki/Total_functional_programming https://en.wikipedia.org/wiki/Total_functional_programming
marcosdumay 6y ago
There is Dhall (https://dhall-lang.org/ https://dhall-lang.org/). The overall loss of expressiveness is surprisingly small, but the number of details you have to work around is annoying.
jefftk 6y ago
If you have a VM that processes opcodes and has no way of (a) adding opcodes to the end or (b) moving backwards in the stream, it won't be Turing complete. I've used a scripting system for a server that was intentionally written this way to bound the harm a misbehaving script could have on the server. RE2 is also designed along these lines https://swtch.com/~rsc/regexp/regexp3.html https://swtch.com/~rsc/regexp/regexp3.html
6gvONxR4sf7o 6y ago
Agreed. It's still just a hypothesis that interesting computing is equivalent to a turing machine and I don't buy it. For basically every program I've built, I could (hypothetically, bugs aside) either prove that it terminates, or it's a program like (forever do "something i can prove terminates"). The space of programs that we actually use seems kinda small. Designing a computing model that only covers what's useful while also making it convenient appears to be a long standing open problem. I'm sooooo curious to see things happen there.
- fnrslvr 6y ago
  > (hypothetically, bugs aside) This is the problem. Interesting computing is some impossibly complex (undecidable, in fact) subset of all computing, that you try to get inside of via the practice of software engineering. Turing's theory of computation provides reasoning tools which allow us to bring rigor to the idea that building correct software that does useful things is generally difficult. > Designing a computing model that only covers what's useful while also making it convenient appears to be a long standing open problem. Per the above point, depending on how you characterize this goal, it's probably impossible to accomplish.
  - 6gvONxR4sf7o 6y ago
    >Interesting computing is some impossibly complex (undecidable, in fact) subset of all computing... I totally disagree here. Or at least I totally disagree that it's a resolved question. All of those nasty problems that face some interesting programs don't face programs we actually write. For example, there is a subset of all turing complete programs that halt. The boundary of that subset isn't decidable, but when I'm writing a program that needs to halt, I write a program I know will halt (why are you pushing to prod if you don't know this program will halt?). Expending a ton of proof effort, I could prove that it halts. So I think the stuff we actually build in practical software is really far from the boundary of the nasty stuff. Suppose I had a programming language that had a termination checker and only allowed programs it can prove will terminate. We know that the termination checker will have to return yes, no, and who knows. It can't just say yes and no without being wrong sometimes, because it's an undecideable problem. Maybe there's some termination checker that can correctly say yes to all the programs we really care about. Since I could prove that my programs terminate, this checker must exist. A language that only allows these programs must not be turing complete. So there must be some non turing-complete languages that can express all the programs I would push to prod at work. Maybe some of those languages are even worth using.
lacker 6y ago
The simplest way to make something not Turing-complete is to put a bound on the resources it can use. Like giving it limited time and/or memory. So you can have a practical, useful, non-Turing-complete language by forcing every function to have a limit on the number of steps it can take. It can be implicit if you want. In practice, most embedded scripting systems use this route, which is why you don't really need a separate language just for non-Turing-completeness.
- fnrslvr 6y ago
  This might get you away from the literal statement of Rice's theorem, but we tend to ask questions about our programs' behaviour across all possible inputs, and these questions tend to remain impossible to solve in general. For example, finding out whether a time-bounded Turing machine outputs 0 all inputs is still undecidable. (coRE-complete, in fact. That's better in some sense than the Pi_2-completeness of the same problem for Turing machines without the time bound, but since neither admits a solution in the form of a computer program, a lot of people would consider the difference an academic curiosity only.)
  - Dylan16807 6y ago
    > For example, finding out whether a time-bounded Turing machine outputs 0 all inputs is still undecidable. Is that a problem? I mean, if you're installing a timeout then haven't you already decided that the answer is "no"?
    - fnrslvr 6y ago
      If the time bound is being put in place in the hopes of being able to automatically analyze the behaviour of the code, then no. I singled out "outputting 0" on every input because it's among the simplest possible specs you could try try to check with the kind of "very powerful semantic analysis" tool the top-level post was hoping for. In practice you probably want to check a more complex spec -- you want your code to solve a specific problem on whatever input it receives -- but if the "always output 0" spec is impossible to automatically check, then what hope do more relevant specs have?
fnrslvr 6y ago
This is kinda part of the promise of regular expressions, context-free grammars, relational algebra, map-reduce and other stream/pipeline-based programming models, and maybe to some extent P-complete things like convex optimizers and programming models based on horn clauses like datalog. Each of these things aims to allow the user to specify a task in a restricted model of computation. In turn, it tends to be possible for the engineer writing the solver to build an engine capable of very radical transformations, optimizations, and analyses, that generally can't be matched by compilers and interpreters for Turing-complete programming languages.
- miltondts 6y ago
  If I want to build a language with those optimizations, what resources could I use?

gpderetta 6y ago

Total Functional Programming is a thing [1]. [1] https://en.wikipedia.org/wiki/Total_functional_programming https://en.wikipedia.org/wiki/Total_functional_programming

marcosdumay 6y ago

There is Dhall (https://dhall-lang.org/ https://dhall-lang.org/). The overall loss of expressiveness is surprisingly small, but the number of details you have to work around is annoying.

jefftk 6y ago

If you have a VM that processes opcodes and has no way of (a) adding opcodes to the end or (b) moving backwards in the stream, it won't be Turing complete. I've used a scripting system for a server that was intentionally written this way to bound the harm a misbehaving script could have on the server. RE2 is also designed along these lines https://swtch.com/~rsc/regexp/regexp3.html https://swtch.com/~rsc/regexp/regexp3.html

6gvONxR4sf7o 6y ago

Agreed. It's still just a hypothesis that interesting computing is equivalent to a turing machine and I don't buy it. For basically every program I've built, I could (hypothetically, bugs aside) either prove that it terminates, or it's a program like (forever do "something i can prove terminates"). The space of programs that we actually use seems kinda small. Designing a computing model that only covers what's useful while also making it convenient appears to be a long standing open problem. I'm sooooo curious to see things happen there.

fnrslvr 6y ago
> (hypothetically, bugs aside) This is the problem. Interesting computing is some impossibly complex (undecidable, in fact) subset of all computing, that you try to get inside of via the practice of software engineering. Turing's theory of computation provides reasoning tools which allow us to bring rigor to the idea that building correct software that does useful things is generally difficult. > Designing a computing model that only covers what's useful while also making it convenient appears to be a long standing open problem. Per the above point, depending on how you characterize this goal, it's probably impossible to accomplish.
- 6gvONxR4sf7o 6y ago
  >Interesting computing is some impossibly complex (undecidable, in fact) subset of all computing... I totally disagree here. Or at least I totally disagree that it's a resolved question. All of those nasty problems that face some interesting programs don't face programs we actually write. For example, there is a subset of all turing complete programs that halt. The boundary of that subset isn't decidable, but when I'm writing a program that needs to halt, I write a program I know will halt (why are you pushing to prod if you don't know this program will halt?). Expending a ton of proof effort, I could prove that it halts. So I think the stuff we actually build in practical software is really far from the boundary of the nasty stuff. Suppose I had a programming language that had a termination checker and only allowed programs it can prove will terminate. We know that the termination checker will have to return yes, no, and who knows. It can't just say yes and no without being wrong sometimes, because it's an undecideable problem. Maybe there's some termination checker that can correctly say yes to all the programs we really care about. Since I could prove that my programs terminate, this checker must exist. A language that only allows these programs must not be turing complete. So there must be some non turing-complete languages that can express all the programs I would push to prod at work. Maybe some of those languages are even worth using.

lacker 6y ago

The simplest way to make something not Turing-complete is to put a bound on the resources it can use. Like giving it limited time and/or memory. So you can have a practical, useful, non-Turing-complete language by forcing every function to have a limit on the number of steps it can take. It can be implicit if you want. In practice, most embedded scripting systems use this route, which is why you don't really need a separate language just for non-Turing-completeness.

fnrslvr 6y ago
This might get you away from the literal statement of Rice's theorem, but we tend to ask questions about our programs' behaviour across all possible inputs, and these questions tend to remain impossible to solve in general. For example, finding out whether a time-bounded Turing machine outputs 0 all inputs is still undecidable. (coRE-complete, in fact. That's better in some sense than the Pi_2-completeness of the same problem for Turing machines without the time bound, but since neither admits a solution in the form of a computer program, a lot of people would consider the difference an academic curiosity only.)
- Dylan16807 6y ago
  > For example, finding out whether a time-bounded Turing machine outputs 0 all inputs is still undecidable. Is that a problem? I mean, if you're installing a timeout then haven't you already decided that the answer is "no"?
  - fnrslvr 6y ago
    If the time bound is being put in place in the hopes of being able to automatically analyze the behaviour of the code, then no. I singled out "outputting 0" on every input because it's among the simplest possible specs you could try try to check with the kind of "very powerful semantic analysis" tool the top-level post was hoping for. In practice you probably want to check a more complex spec -- you want your code to solve a specific problem on whatever input it receives -- but if the "always output 0" spec is impossible to automatically check, then what hope do more relevant specs have?

fnrslvr 6y ago

This is kinda part of the promise of regular expressions, context-free grammars, relational algebra, map-reduce and other stream/pipeline-based programming models, and maybe to some extent P-complete things like convex optimizers and programming models based on horn clauses like datalog. Each of these things aims to allow the user to specify a task in a restricted model of computation. In turn, it tends to be possible for the engineer writing the solver to build an engine capable of very radical transformations, optimizations, and analyses, that generally can't be matched by compilers and interpreters for Turing-complete programming languages.

miltondts 6y ago
If I want to build a language with those optimizations, what resources could I use?