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