[simcop2387]

The big problem with that is that if a language is decidable it can't be Turing complete. That means that a large number of useful programs are just not going to be expressible. That said for something g like this it's a perfect fit to have it be decidable.

[chowells]

There are no useful programs that require Turing completeness. That's basically by definition. Turing completeness is what allows programs to have non-productive infinite loops. Any system that guarantees productivity isn't Turing complete. All useful algorithms are productive. The only thing you can do with a non-productive algorithm is convert electricity to heat.

[saghm]

I took a course in college where we used Coq to build up an imperative programming language, and I waa surprised how much you could do (i.e. essentially anything you needed to) with a non-Turing complete language. I think that the traditional computer science curriculum makes such a big deal about Turing machines (and not necessarily wrongly so) that students just assume that Turning completeness is a natural goal to strive for rather than just a property with tradeoffs, just like any other property. It certainly doesn't help that it seems harder to create a language that's not Turing complete than one that is, at least if you aren't explicitly trying to avoid it; just look at all the random things that have been discovered to be accidentally Turing complete over the years.

[TelmoMenezes]

> Any system that guarantees productivity isn't Turing complete. All useful algorithms are productive.

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...

[lmm]

> 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.

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.

[TelmoMenezes]

> 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.

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.

[lmm]

> 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.

They're unproven, not believed to be unprovable. (Indeed, almost all practical programs make at least some effort to offer evidence and informal arguments for their correctness, via tests, comments on unsafe constructs, and so on).

> 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.

This is meaningless woo.

[TelmoMenezes]

> They're unproven, not believed to be unprovable.

A decidable language (let's say Ld) is less powerful than a Turing-complete language (Lt). This means that there are some computations that can be expressed in Lt but not in Ld, and that there are some problems that can be solved in Lt but not in Ld. These are theorems of theoretical computer science. I don't believe anyone has a clear idea of the practical implications of this limitation, and how many of the algorithms in current use are only possible in Lt.

My guess is that the complexity of the software in use nowadays vastly exceeds our ability to do such an analysis, but maybe you know something I don't. Otherwise, while it is true that they are not believed to be unprovable, it is also true that they are not believed to be provable.

> This is meaningless woo.

I'm not sure I should reply to this, because it is just name calling, but for other people reading this (and you, if you're still interested): people who study artificial creativity and related fields such as Artificial Life take these ideas seriously and have interesting philosophical definitions and mathematical formalisms to address them. I have been to conferences sponsored by serious universities and other organisations such as ACM and IEEE where ideas such as the generative power of the Mandelbrot set are seriously discussed. There are several attempts to quantify creativity and to connect the idea of creativity with computer science.

It is important to not have a mind so open that the brain falls off, but I suggest that you may be going too far in the opposite direction.

[tom_mellior]

> > 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

> 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.

[lmm]

But we wouldn't want to just leave such a theorem prover running indefinitely. Far more practical to have it check all possible proofs of length up to n (trivial to do in a total language), or at most run it for a particular number of days, months or years. At some point you do end the experiment.

[tom_mellior]

Sure. You usually run the prover with a timeout. The point is, this is a practical example of running a program where you cannot predict whether it will "work" or not. Additionally, when you reach the timeout, you will not have gained any information, i.e., the process is not "productive" in the sense discussed above.

Edit: Can't reply to your reply. Interesting. Yes, true, "there is no proof of length < N" is some information, but it's not information that tells you anything about the provability of your formula. It's not productive information. You can keep trying, but you won't be able to overturn the semidecidability of first-order logic in a Hacker News comment thread.

[simcop2387]

So I might have made this a bit confusing too by conflating the two things in my original post. The real thing is that there are a lot of undecidable programs that don't require Turing completeness. And a lot of those useful programs are undecidable, an example of a really simple undecidable program:

    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"

That program, because it might loop indefinitely isn't decidable and isn't possible to describe with Viper by design. This kind of program is pretty analogous to basically every program that communicates with the network, user, or some other external system.

[colanderman]

"Undecidability" doesn't apply to interactive systems. Inputs must be finite: https://en.wikipedia.org/wiki/Undecidable_problem In your example, the input (an infinite stream of strings not equal to "Ralph") is not finite.

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.

[E6300]

It's not a given that the input is infinite. If the used types in "Rob" then goes away forever, the program will neither terminate nor process an infinite number of non-"Ralph" strings. It will sit just sit there waiting (possibly in a loop, possibly not) for a hardware interrupt that will never arrive.

[colanderman]

For decidability to apply, the input needs to be known a priori in its entirety. Decidability is a mathematical statement about natural numbers (or any other countably infinite set); it has absolutely nothing to do with "paused" input or any notion of "interactivity".

The type of behavior you're concerned with does on the other hand fall squarely in the realm of temporal logics (e.g. TLA+), which do concern themselves with interactivity and indeterminate pauses. For example, the statement "so long as the user eventually inputs the string 'Ralph', the algorithm eventually terminates" is decidable for any finite state machine.

In other words, if you limit your interactivity logic to that expressible by a finite state machine with decidably halting transitions, congratulations, you are writing decidably halting programs, even though they don't "halt" in the temporal sense. It's always possible to tell whether they will halt for a given input by completely analyzing the state space.

[PKop]

Isn't this a question of upper-bound on input? Not specific examples that are less than the upper bound..

[Risord]

So how non-turing completeness work with infinite streams?

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?

[tom_mellior]

Coq is not Turing complete but has support for coinductive data types (= infinite streams) and (co-)recursion over them.

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.

[pron]

If you have support for coinductive data types then you are Turing complete. Proof: you can simulate a Turing machine. However, Coq's term language is not Turing complete, meaning that every syntactic element in Coq evaluates to a terminating computation.

[lmm]

> 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.

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.

[colanderman]

See my sibling comment. Decidability by definition does not apply to infinite inputs (i.e., it is a nonsensical question to ask, like "what is the square root of potato?"). Some proof languages like Coq implicitly extend decidability to extend to infinite streams with finite representations (think generative regular expressions or state machines).

[dismantlethesun]

It won't. It will instead operate over the first googol items and then require a restart.

[mycall]

I miss line numbers

[dragonwriter]

> This kind of program is pretty analogous to basically every program that communicates with the network, user, or some other external system.

Not really; it's quite possible, and often desirable, to do that without potentially infinite loops.

[simcop2387]

So how do you do that for the server side of things? Only accept a certain number of connections before you have to completely shut down and restart the server? How do you do the restart without the infinite loop somewhere?

[swsieber]

Exactly - you want timeouts, exponential backoff, etc. You want to know what happens if a network failure happens - you don't want to retry ad nauseam.

[sillysaurus3]

Some of the most reliable programs are those without exponential backoff and which retry infinitely in network failure situations. `ping` is one example.

[swsieber]

And yet I'd be completely fine with a ping that was capped to running for no more than a week. YMMV though.

And more to the point, you don't want a program that goes on forever in a setup like ethereum. I guess your rebuttal was called for since the initial point was a little hyperbolic.

[sillysaurus3]

How?

[Shorel]

The old good O-Machine.

[dnautics]

> All useful algorithms are productive.

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.

[avaer]

Doesn't any program that processes interactive/network IO require an infinite loop?

Are those programs not useful?

[dragonwriter]

> Doesn't any program that processes interactive/network IO require an infinite loop?

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.

[mbrock]

It seems that a better solution is to guarantee that each step of such an unbounded loop is bounded, and clearly distinguish these types of processes.

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.

[eberkund]

No, they can use interrupts instead.

[avaer]

I don't understand how that avoids looping. If your program doesn't loop waiting for interrupts, it has terminated. So it won't be getting those interrupts.

[dom0]

AIUI smart contracts mean that a ton of nodes has to execute this code, so making the language of the code as weak as possible would seem like an important design goal to me from a langsec PoV.