10 PRINT "Enter your name"
20 INPUT NAME$
30 PRINT "Hello ", NAME$
40 IF NAME$ <> "Ralph" THEN
41 GOTO 10
42 END IF
50 PRINT "Goodby Ralph"
Instead, think of an interactive system as a finite state machine. The question to ask then is, do any of my state transitions require a Turing-complete language to express? In 99.999% of all software ever written the answer is "no". Inability to prove termination is almost certainly a software bug or flaw in the design. The theoretical exceptions are exotic algorithms for which termination is not provable; the practical exceptions are probabilistic algorithms for which termination is not in fact guaranteed (e.g. a naïve hash table implementation).
The difference is important. A state machine, even one that represents a non-terminating system over infinite input (e.g. a web server), still can be reasoned about. This is exactly the domain of tools like TLA+, which can answer questions such as, "is my system guaranteed to always eventually take action X given input Y?" and "is my system guaranteed to never terminate?" But to be able to answer such questions, it's a prerequisite that the transitions between states do in fact terminate.
Many practical applications (like this) are working with possibly infinite stream of user inputs / requests etc. If we can guarantee that our server, browser or game application just stops eventually we know that something is wrong. However we like to guarantee that our application won't work infinitely with single request / input / time tick. So does this say that we want avoid using turing complete language mostly but turing complete part need to be handled somewhere maybe outside of our code? Something like how Haskell works with side effects. What you think?
Simplifying a lot, it has a syntactic "guard condition" that says that you must produce some result before you're allowed to make a recursive call. For example, you can map over an infinite stream because a map produces a result for each element of the input stream. Unlike Haskell, you cannot write a fold over an infinite stream because you would need to look at all elements before producing a result.
So if you can structure your system as a transformation from an infinite stream of requests to an infinite stream of responses, you're fine in Coq even though it is not Turing complete.
The intuition is that, just like in Haskell, you don't actually end up doing an infinite computation if only a finite part of the final result is ever requested.
Yes. E.g. you might have most of your logic in a turing-incomplete per-tick or per-request function, and then a single explicitly "unsafe" infinite loop at top level. In a language like Idris this happens naturally - you just have an explicit distinction between total and not-necessarily-total functions.
Not really; it's quite possible, and often desirable, to do that without potentially infinite loops.
Are those programs not useful?
No.
I mean, there are lots of common uses of unbounded loops in that domain, but any of them could be replaced with maximum-bounded loops with sufficient large bounds and be unnoticeably different in practice, mostly cutting off (largely pathological) edge cases.
For example, a kernel's scheduler should run indefinitely, but each scheduling step should be bounded. Ideally we would specify the scheduler loop as a non-terminating yet "productive" process.
But it does not follow that all useful algorithms can be implemented on a language that "guarantees productivity". Turing proved that the halting problem cannot be solved on a Turing machine. This opens the possibility for the existence of programs that might be "productive" in your sense, but might also never stop, and it is not possible to know in advance.
> The only thing you can do with a non-productive algorithm is convert electricity to heat.
I am not convinced of this at all. Perhaps true if you are talking about banking systems or web applications, but probably not true if you are talking about AI. Intermediary states of an endless computation might be interesting. Maybe this is a way to obtain unbounded creativity. Maybe this is the way to build minds. We don't know enough.
A more general observation: I find that we live in an era that is too obsessed with productivity at the cost of fundamental research, dreaming and imagination. I am convinced that the latter mindset is the only one that can bring qualitative changes to our culture and civilisation, and I think that our long-term survival depends on such qualitative jumps.
Of course, I also understand that someone has to take care of the plumbing...
Maybe. I struggle to imagine a practical case where we want to run a program that we didn't and couldn't know whether it worked though.
> I am not convinced of this at all. Perhaps true if you are talking about banking systems or web applications, but probably not true if you are talking about AI. Intermediary states of an endless computation might be interesting. Maybe this is a way to obtain unbounded creativity. Maybe this is the way to build minds. We don't know enough.
This is ridiculous reasoning. "We don't understand X, we don't understand Y, therefore X might be related to Y."
> A more general observation: I find that we live in an era that is too obsessed with productivity at the cost of fundamental research, dreaming and imagination. I am convinced that the latter mindset is the only one that can bring qualitative changes to our culture and civilisation, and I think that our long-term survival depends on such qualitative jumps.
> Of course, I also understand that someone has to take care of the plumbing...
Choosing to look at non-halting programs rather than halting programs is like choosing to look at crystal energy instead of nuclear fusion. A certain amount of willingness to question baseline assumptions is valuable, but I think our long-term survival depends far more on being willing to acknowledge the fundamental results of the field and put in the hard engineering work necessary to achieve things under the constraints of reality, rather than trying to wave them away.
The vast majority of the programs used in real life are not formally proven and are written in Turing complete languages. That is already the world you live in.
> This is ridiculous reasoning. "We don't understand X, we don't understand Y, therefore X might be related to Y."
I didn't say that.
Notice that a (very simplified) model of the human brain, the recurrent neural network, is already Turing complete. Notice also that humans (and Darwinian evolution, for that matter) display a capacity for creativity that has not been successfully replicated by AI efforts yet. Notice further that non-halting computations (e.g. infinitely zooming a Mandelbrot set) are the closest thing we have to unbounded creativity.
Maybe I'm wrong, of course.
> I struggle to imagine a practical case where we want to run a program that we didn't and couldn't know whether it worked though.
First-order theorem proving is a very practical case. Proof in first-order logic is "recursively enumerable", which means that we can write provers that, given a formula F, produce a proof of F in finite time if such a proof exists. But in general we don't know if a proof exists or how long it will take to find it. So if we start a prover, it will just sit there and not look "productive" until it either returns a proof or we kill it because we're tired of waiting.
I'm gonna have to call "not quite" on that one. There's some zeroth-order truth and appeal to that statement, but there are certainly stochastic algorithms that have virtually guaranteed to be awesome, but have a nonzero likelihood, unbounded worst case scenario.