Rice's Theorem isn't as strong as you say it is. What it says is that there exist programs that it's impossible to prove whether or not they have specific non-trivial properties. But there still exist many programs where we can prove their correctness / incorrectness. What's more, I'd argue that if you're writing code whose behaviour is literally undecidable, you're doing something wrong, unless you're doing it for research purposes or something like that.

> Rice's Theorem isn't as strong as you say it is

It is very strong: its corollary is there is no general algorithm to build Turing Machines with arbitrary non-trivial properties (if there was such an algorithm we could use it to build a TM that solves the halting problem)

So for any non-trivial property the only way to build a TM with this property is to use some ad-hoc method (as there is no general algorithm) - but how do we know the TM we've just built really holds the property we wanted it to? There is no way to verify it due to Rice's theorem.

Quoting from Wikipedia about Rice's theorem:

> for any non-trivial property of partial functions, no general and effective method can decide whether an algorithm computes a partial function with that property

This basically translates to "for each non-trivial property P, there exists a program x for which it is undecidable if x has the property P", or "∀P ∃x such that it's undecidable if x has property P".

Notice that in this statement, programs are quantified using an "exists", not a "forall". Something similar holds for what you said here:

> its corollary is there is no general algorithm to build Turing Machines with arbitrary non-trivial properties

Translated to logic, this becomes "for every program y which takes as input a property and outputs a Turing Machine, there exists a property P such that the y(P) does not have property P", or "∀y ∃P y(P) does not have property P".

Because this statement uses "exists" on the property, it does not rule out the existence of a y which works for most properties P that we'd care about. It only rules out one that works for all properties.

As a simple example where it's possible to prove a non-trivial property, take the property "x is the identity function". This is a non-trivial property, because it is not true about all programs, nor is it false about all programs. And it is trivial to prove that the function "(n) => n" satisfies this property.

Now, I additionally think that most practical programs can have their correctness / incorrectness proven. My reason for this belief is that generally, I expect coders to understand why the code they're writing should work. If nobody understands why the code works, I'd generally consider that a bug, or at least a major code smell. But if the programmer actually understands why the code works, and hasn't made any mistakes, then in principle their understanding could be converted into a proof, because proofs are more or less just correct reasoning, but written out formally. Of course, it would still be very hard, but it's not "provably impossible".

Edit: minor text change

> Because this statement uses "exists" on the property, it does not rule out the existence of a y which works for most properties P that we'd care about. It only rules out one that works for all properties.

Translated: there exists a computational model weaker than TM but strong enough to implement programs we care about.

Unfortunately, we don't know such computational model and we know empirically surprisingly many problems require a TM (ie. surprisingly many languages are accidentally Turing complete)

Making a system Turing-complete, even accidentally, does not make it proof against analysis. A system or input for the system may be built out of parts that could be used to make an undecidable system. But that does not mean you can only build undecidable systems with those parts.

It is in fact extremely common to build wholly deterministic machines out of the same parts as our unreliable computers, that are correct by construction. And they may implement a Turing-complete language and still be wholly deterministic, just by limiting the input to what can be proven deterministic in a strictly limited time. Again, this is normally by construction, where the proof is always trivial.

Such a proven-correct system can model literally any space-constrained algorithm.

> It is in fact extremely common to build wholly deterministic machines out of the same parts as our unreliable computers, that are correct by construction.

It is neither common nor easy but actually provably impossible. Please read this piece carefully: https://pron.github.io/posts/correctness-and-complexity

Yet, it is done, thousands of times every day, all over the world.

You must be misunderstanding the work if you believe that what is being done routinely is impossible.

> You must be misunderstanding the work if you believe that what is being done routinely is impossible.

Quite possibly I don't understand what you mean by "work". If by "work" you mean creating provably correct software then no, it is not done routinely.

The work is the paper you cited.

People create wholly deterministic state machines all the damn time.

> People create wholly deterministic state machines all the damn time.

What do you mean by "wholly deterministic"?

All possible states are well-understood, all possible paths through states are mapped.

You can buy an 8-bit adder/accumulator from a catalog.

I just want to point out that you don't need to know the precise bounds of such a computational model to prove things about your programs. There already exist Turing-complete programming languages where you can prove non-trivial properties about your program and which have had practical applications, for example F* and its use in Project Everest.

https://project-everest.github.io/

https://www.fstar-lang.org/

Just having a language that allows you to prove things does not mean it is possible to prove them.

We still don't know if it is possible to build a provably correct multi-tasking OS or a web browser without security vulnerabilities. If it was easy we would already have one written in FStar or Idris.

While admiring all the work done by Project Everest - the fact is that it is a multi-year project (I first read about it about 3-4 years ago and it was already under way) with a very limited scope - it is more of an evidence of difficulties of writing correct software.

This still doesn't exclude the existence of a general method for a well-behaved subset of Turing machines. It is the model of Turing machines that is too powerful.

There are two problems with this:

1. Even for as weak computational model as FSM the problem of verifying its correctness is intractable (NP-hard). And modularisation does not help.

2. We don't know any weaker computational model that is strong enough to be viable for the problems we want to solve and still weaker than TM. It is well known that it is surprisingly easy for a language to be (accidentally) Turing complete.

Yet languages with totality checkers and coinduction like Idris exist. These allow you to make useful but provably terminating programs. Humans are able to construct these termination proofs, though presumably not for all programs.

In practice, this means that the reductive take of Turing completeness, the halting problem and Rice's theorem is misleading in some way.

Yes, there is no general algorithm for constructing termination proofs for any arbitrary Turing machine. But there are clearly classes of problems for which a biological computer (a human) is able to construct termination proofs and proofs regarding other semantic properties.

It is not necessary to verify that random presented machines have some property. It suffices that we can reliably construct machines that perform a desired function and have the desired property.

> It suffices that we can reliably construct machines that perform a desired function and have the desired property.

See above - there is no reliable procedure (algorithm) that would allow you to do that.

Rice’s theorem says no such thing. Rice’s theorem tells you you can’t necessarily prove you’ve built a flawless system, not that you can’t build a flawless system. You can build a perfect program even if you can’t necessarily then know you have.

Perhaps you interpreted my post to suggest that you could build a machine that verifies that any arbitrary software run on it never enters an invalid state? If so, I agree, that is not possible. I made a minor edit to make it clear what I’m talking about.

> Rice’s theorem tells you you can’t prove you’ve built a flawless system, not that you can’t build a flawless system.

If you think about it - it is the same: how do you know the system you just built is flawless?

You don't, but it's still flawless. My point was that it was theoretically, not practically possible. So your retort that it's not practically possible is kind of missing the point.

My point is that it is _theoretically_ not possible: there is no algorithm that would allow you to build a TM implementing arbitrary requirements.

You have to use ad-hoc methods but then it is not possible to know your ad-hoc method is correct!

So by "flawless" you can only mean "having some property but we cannot say what property it is".

Edit: added "flawless" definition

I'm not sure you're getting this. Let's say you want to build a video chat application with all of the same features as Zoom and not a single bug. That is, in fact, possible. Nothing about Rice's Theorem says you can't build a program without bugs. You can build a flawless video chat application. You won't, but you can. How? Very easy. Every time you're about to write code with a bug, don't. Write that same code but without the bug.

> Every time you're about to write code with a bug, don't. Write that same code but without the bug.

This procedure (algorithm) is ill-defined (is not realisable by a TM) as it would require verifying two things:

a) the code you are about to write has a bug (ie. has a specific property)

b) the code you wrote does not have a bug (ie. has a specific property)

Rice's theorem says both are impossible.

Maybe moving to a specific instance of Rice's theorem is clearer. My point is that while he can't solve the halting problem—i.e. he can't reliably determine whether any arbitrary program will halt—an infallible programmer can reliably write his own programs such that they always halt.

So, to go back to the original point, you can't reliably determine the correctness of every possible program. But you could, if you were not prone to error like all humans, always write your own programs such that they are always correct.

No.

From the fact that we know how to write programs that halt you cannot deduce we know how to write programs with arbitrary (or even just useful) property, because there is no general procedure to do that.

In other words: you cannot use the algorithm of writing programs that halt to write programs computing nth digit of Pi :)

Because you built it in a series of steps, exactly zero of which introduced any undecidability.

See above - there is no reliable procedure (algorithm) that would allow you to build a TM with arbitrary properties (ie. implementing arbitrary requirements).

Programs don't have to have Turing-complete behavior. Compilers do, but not every program needs to implement uncomputable behavior on its inputs.

Actually it's the other way around:

In reality most interesting programs accept Turing complete languages - albeit not formally specified :)