How many modern programmers hold this mistaken belief? It's false -- the Turing Halting problem (https://en.wikipedia.org/wiki/Halting_problem) demonstrates that one cannot establish that a non-trivial program is "provably correct."
It seems the OP got carried away with his rhetoric, and the way he put it is simply wrong.
That is a very common but incorrect misinterpretation of the halting problem.
The halting problem says that there exist programs that cannot be proven correct; it says that for any property you want to prove computationally, no program can give you an answer for every last program. It doesn't say anything about "non-trivial" programs. In particular, if you write programs with awareness of the halting problem in mind, you can write extremely complicated programs that are provably correct.
One straightforward way to do this is with a language that always halts. The proof assistant Coq is based on such a language, and it's powerful enough to write a C compiler: http://compcert.inria.fr/
It is certainly correct that you can't stuff an arbitrarily vexatious program through a proof assistant and get anything useful on the other side. But nobody is interested in proving things about arbitrarily vexatious programs; they're interested in proving things about programs that cooperate with the proof process. If your program doesn't want to cooperate, you don't need an exact answer; you might as well just say "No, I don't care, I'm not trusting you."
Right. This is a bogus complaint about proof of correctness.
The way you prove halting is to find some integer measure for each loop (like "iterations remaining" or "error being reduced") which decreases on each iteration but does not go negative. If you can't find such a measure, your program is probably broken. (See page 12 of [1], the MEASURE statement, for a system I built 30 years ago which did this.)
The measure has to be an integer, not a real number, to avoid Zeno's paradox type problems. (1, 1/2, 1/4, 1/8, 1/16 ...)
On some floating point problems, with algorithms that are supposed to converge, proving termination can be tough. You can always add an iteration counter and limit the number of iterations. Now you can show termination.
Microsoft's Static Driver Verifier is able to prove correctness, in the sense of "not doing anything that will crash the kernel", about 96% of the time. About 4% of the time, it gives up after running for a while. If your kernel driver is anywhere near close to undecidability, there's something seriously wrong with it.
In practice, this is not one of the more difficult areas in program verification.
Pascal-F is interesting and not in my collection. What were most useful or interesting things you did with it? And does it have any use today in modern Pascal-like languages (maybe Modula-2 revision)?
> It doesn't say anything about "non-trivial" programs.
No, but its source does. The source for the Turing Halting problem is Gödel's incompleteness theorems, which do specify that the entities to which it applies are non-trivial. The Turing Halting problem, and Gödel's incompleteness theorems, are deeply connected.
> One straightforward way to do this is with a language that always halts.
That doesn't avoid the halting problem, it only changes the reason for a halt. And it cannot guarantee that that program will (or won't) halt, if you follow -- only its interpreter.
> In particular, if you write programs with awareness of the halting problem in mind, you can write extremely complicated programs that are provably correct.
You need to review the Turing Halting problem. No non-trivial computer program can be proven correct -- that's the meaning of the problem. It cannot be waved away, any more than Gödel's incompleteness theorems can be waved away, and for the same reason.
> The source for the Turing Halting problem is Gödel's incompleteness theorems, which do specify that the entities to which it applies are non-trivial. The Turing Halting problem, and Gödel's incompleteness theorems, are deeply connected.
Gödel doesn't say anything about "non-trivial" any more than Turing does. His first theorem is a "there exists at least one statement" thing, just like the halting problem. Like the halting problem, the proof is a proof by construction, but that statement is not a statement that anyone would a priori are to prove, just like the program "If I halt, run forever" is not a program that anyone would particularly want to run. So while yes, they're deeply connected, from the point of view of proving actual systems correct, it's not clear they matter. And neither theorem says anything about "non-trivial" statements/programs (just about non-trivial formalizations and languages).
Gödel's second theorem is super relevant, though: it says that any consistent system cannot prove its own consistency. But that's fine. Coq itself is implemented in a Turing-complete language (ML), not in Coq. It would be nice if we could verify Coq in Coq itself, but since Gödel said we can't, we move on with life, and we just verify other things besides proof assistants. (And it seems to be worthwhile to prove things correct in a proof assistant, even without a computer-checked proof of that proof assistant's own correctness.)
This is not waving away the problem, it's acknowledging it and working within the limits of the problem to do as much as possible. And while that's not everything, it turns out a lot of stuff of practical importance -- perhaps everything of practical importance besides proving the system complete in its own language -- is possible.
Quote: "Rice's theorem generalizes the theorem that the halting problem is unsolvable. It states that for any non-trivial property, there is no general decision procedure that, for all programs, decides whether the partial function implemented by the input program has that property. (A partial function is a function which may not always produce a result, and so is used to model programs, which can either produce results or fail to halt.) For example, the property "halt for the input 0" is undecidable. Here, "non-trivial" means that the set of partial functions that satisfy the property is neither the empty set nor the set of all partial functions."
Quote: "Gödel's incompleteness theorems are two theorems of mathematical logic that establish inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic."
> It would be nice if we could verify Coq in Coq itself ...
I was planning to bring this issue up, but you've done it for me. The simplest explanation of these two related theorems involves the issue of self-reference. Imagine there is a library, and a very conscientious librarian wants to have a provably correct account of the library's contents. The librarian therefore compiles an index of all the works in the library and declares victory. Then Gödel shows up and says, "On which shelf shall we put the index?"
In the same way, and for the same reason, non-trivial logical systems cannot check themselves, computer languages cannot validate their products (or themselves), and compilers cannot prove their own results correct.
> And it seems to be worthwhile to prove things correct in a proof assistant, even without a computer-checked proof of that proof assistant's own correctness.
Yes, unless someone is misled into thinking this means the checked code has been proven correct.
> This is not waving away the problem ...
When someone declares that a piece of code has been proven correct, in point of fact, yes, it is.
> for any non-trivial property, there is no general decision procedure that, for all programs
> all but the most trivial axiomatic systems
This is about non-trivial properties on arbitrary programs, and non-trivial axiomatic systems proving arbitrary statements. It is not about non-trivial programs or non-trivial statements.
Rice's theorem states that, for all non-trivial properties P, there exists a program S where you cannot compute P(S). (The Wikipedia phrasing puts the negative in a different spot, but this is de Morgan's law for quantifiers: ∀P ¬∀S P(S) is computable = ∀P ∃S ¬ P(S) is computable.)
Gödel's first theorem is that, for all non-trivial formalizations P, there exists a statement S where you cannot prove P in S.
You are claiming, for all non-trivial properties P, for all non-trivial programs S, you cannot compute P(S); for all non-trivial formalizations P, for all non-trivial statements S, you cannot prove P in S.
This is not what Rice's or Gödel's theorems are, and not what the texts you quoted say.
> Then Gödel shows up and says, "On which shelf shall we put the index?"
You keep it outside the library. The index tells you where every single book is, other than the index.
In particular, Gödel claims that, if the index has any chance of being correct, it must be outside the library. The fact that Coq cannot be proven in Coq does not decrease our confidence that it is correct; in fact, Gödel's second theorem means that if it could be proven in itself, we'd be confident it was wrong!
>> Then Gödel shows up and says, "On which shelf shall we put the index?"
> You keep it outside the library. The index tells you where every single book is, other than the index.
This approach would have saved Russell and Whitehead's "Principia Mathematica" project, would have placed mathematics on a firm foundation, but it suffers from the same defect of self-reference -- it places the index beyond validation. Russell realized this, and recognized that Gödel's results invalidated his project.
> The fact that Coq cannot be proven in Coq does not decrease our confidence that it is correct;
Yes, true, but for the reason that we have no such confidence (and can have no such confidence). We cannot make that assumption, because the Turing Halting problem and its theoretical basis prevents it.
Quote: "Gödel hammered the final nail home by being able to demonstrate that any consistent system of axioms would contain theorems which could not be proven. Even if new axioms were created to handle these situations this would, of necessity, create new theorems which could not be proven. There's just no way to beat the system. Thus he not only demolished the basis for Russell and Whitehead's work--that all mathematical theorems can be proven with a consistent set of axioms--but he also showed that no such system could be created." (emphasis added)
> Russell realized this, and recognized that Gödel's results invalidated his project.
One particular project. The specific project of formalizing mathematics within itself is unachievable. That doesn't mean we've stopped doing math.
And this is in fact the approach modern mathematics has taken. The fact that one particular book (the proof of mathematics' own consistency) can't be found on the shelves doesn't mean there isn't value in keeping the rest of the books well-organized.
> Yes, true, but for the reason that we have no such confidence (and can have no such confidence). We cannot make that assumption, because the Turing Halting problem and its theoretical basis prevents it.
No! Humans aren't developed in either Coq or ML. A human can look at Coq and say "Yes, this is correct" or "No, this is wrong" just fine, without running afoul of the halting problem, Gödel's incompleteness theorem, or anything else. The fact that you can have no Coq-proven confidence in Coq's correctness does not mean that you can have no confidence of Coq's correctness.
(Of course, this brings up whether a human should be confident in their own judgments, but that's a completely unavoidable problem and rapidly moving to the realm of philosophy. If you are arguing that a human should not believe anything they can convince themselves of, well, okay, but I'm not sure how you plan to live life.)
This is like claiming that, because ZF isn't provably correct in ZF (which was what Russell, Whitehead, Gödel, etc. were concerned about -- not software engineering), mathematicians have no business claiming they proved anything. Of course they've proven things just fine if they're able to convince other human mathematicians that they've proven things.
>> Russell realized this, and recognized that Gödel's results invalidated his project.
> One particular project.
A mathematical proof applies to all cases, not just one. Gödel's result addressed Russell's project, but it applies universally, as do all valid mathematical results. Many mathematicians regard Gödel's result as the most important mathematical finding of the 20th century.
> That doesn't mean we've stopped doing math.
Not the topic.
> A human can look at Coq and say "Yes, this is correct" or "No, this is wrong" just fine, without running afoul of the halting problem, Gödel's incompleteness theorem, or anything else.
This is false. If the Halting problem is insoluble, it is also insoluble to a human, and perhaps more so, given our tendency to ignore strictly logical reasoning. It places firm limits on what we can claim to have proven. Surely you aren't asserting that human thought transcends the limits of logic and mathematics?
> Of course they've proven things just fine if they're able to convince other human mathematicians that they've proven things.
Yes, with the caution that the system they're using (and any such system) has well-established limitations as to what can be proven. You may not be aware that some problems have been located that validate Gödel's result by being ... how shall I put this ... provably unprovable. The Turing Halting problem is only one of them, there are others.
> A mathematical proof applies to all cases, not just one. Gödel's result addressed Russell's project, but it applies universally, as do all valid mathematical results.
What? I have no idea what you mean by "applies universally" and "all valid mathematical results."
A straightforward reading of that sentence implies that Pythagoras' Theorem is not a "valid mathematical result" because it applies only to right triangles. That can't be what you're saying, is it?
I am acknowledging that Gödel's second theorem states that any mathematical system that attempts to prove itself is doomed to failure. I am also stating that Russell's project involved a mathematical system that attempts to prove itself. Therefore, Gödel's second theorem applies to Russell's project, but it does not necessarily say anything else about other projects.
> Many mathematicians regard Gödel's result as the most important mathematical finding of the 20th century.
So what? This is argumentum ad populum. How important the mathematical finding is is irrelevant to whether it matters to the discussion at hand.
> This is false. If the Halting problem is insoluble, it is also insoluble to a human
OK, so do you believe that modern mathematics is invalid because Russell's project failed?
No, I don't believe that the future is languages that are not Turing-complete, mostly because halting is not the property most people care about. I believe that a large part of the future will be languages that are not Turing-complete, for applications where that's appropriate (e.g., C compilers) but not where it's not (e.g., interpreters). I also don't think that "well, that's how we've always done it" is a particularly compelling argument given how young the field of programming languages is.
For instance, another wonderful example of requiring code to cooperate with the proof process is Google's Native Client. NaCl doesn't care about halting; what it cares about is that the code in question only accesses its own memory, or makes specific pre-defined calls into the supervising code. You can do this with hardware support (and they did, with segmentation, where available), but you can also do this with software support.
The NaCl technique is straightforward. You're required to lay out your assembly so that every 32-byte alignment boundary separates instructions; you must insert NOPs as necessary. Any fixed read, write, or jump must be within an address within a mask (or to a predefined address in privileged code), and any computed read, write, or jump must be immediately preceded, within the same 32-byte block, by a mask operation on the relevant register. For data, the mask enforces that only data is accessed; for jumps, the mask enforces that the jump target is within the code area and also 32-byte aligned.
Now you've proven a fairly complicated property of the code, that control flow never escapes to privileged code except at well-defined entry points. Doing so on arbitrary x86 would be impossible (unless you resort to binary translation), but this is a very minor modification to arbitrary x86, and a regular C compiler can be easily modified to emit it. The resulting restricted variant of x86 remains Turing-complete.
And it is entirely reasonable for the NaCl verifier to say "Uh, what are you doing, please try again" if presented with code that is technically non-malicious but does not follow the rules. The NaCl verifier doesn't claim to detect malicious code (that's the antivirus problem, and unsolvable). It claims to take code that makes a specific promise about not being malicious, and verifies that property.
"halting is not the property most people care about"
I agree that non-Turing complete languages are hugely interesting and likely to be more important as we go forward.
But not for this reason. Most of the non-trivial properties people do care about can be used to tell you if a program is going to halt in a finite amount of time. Want an upper bound on memory? This program doesn't have one? Well, then it never halts. It has one? Well, then we know it halts or loops within 2^bits steps - run it for that many steps and you know which.
I think non-Turing-complete will prove interesting because our programs are currently described in Turing complete languages, but run in more constrained contexts anyway. A program that always halts after running for 2^100 steps is not Turing complete. A program that halts if it tries to use more than 2^100 bytes of memory is not Turing complete. Applying these constraints in this way doesn't help us with analysis much, but it hints that we can probably find other ways to constrain our programs which won't get in the way of what we're trying to accomplish, and it's quite possible that some of those will let us build languages more amenable to analysis (and further possible that the gains in analysis will make up for a limited amount of getting-in-the-way).
I don't know where this thinking gets us. My computer, once I disconnect it from the internet, is actually a finite state machine and not a Turing machine, which I think you acknowledge. How does that help with anything?
If my program uses one kebibyte of memory -- no I/O and harddrive, then it loops or halts within 2^(2^10) steps. For me to detect that, in general I need to store a history of length 2^(2^10), which is more than 10^300. That's 10^301 bytes that I need to detect if a 1kb RAM program loops.
It is a proof that we can get what we need to done in a language that is not Turing complete. The hope would be that there is some sweet spot we can find wherein we can say things that are dramatically more useful than "it will finish inside 2^(2^100) steps" without impacting usability tremendously more than "it won't use more than a kebibyte of memory" - which is already enough to defang the theoretical objection.
http://research.google.com/pubs/archive/34913.pdf section 4 discusses performance: "The worst case performance overhead is [the SPEC2000 benchmark named] crafty at about 12%, with other benchmarks averaging about 5% overall." For some applications, there is no slowdown or even a minor speedup because of weird caching behavior and alignment.
I haven't seen this used for a general-purpose OS distro (I suppose you'd use it for running a VM-like thing as an unprivileged user, without access to any hardware features) but I agree it would be cool.
Oh, perhaps I misunderstood, then. Is it not likely that the vast majority of C/C++ userspace programs could survive this change-in-compiler-output-to-meet-restriction without functionality impact?
Yes, you could apply this change in compiler output without functionality impact to existing userspace applications. But you'd have to recompile everything, and it's not clear how it'd be useful; part of the question is what the privileged interfaces should be.
For Chrome this is useful because they want Chrome itself to be an unprivileged application, and they want to be essentially a recursive kernel to untrusted web content: there are multiple "users" (websites) that shouldn't be able to access each other's content, and certainly shouldn't be able to mess with the browser itself, and they get a restricted filesystem-like thing, screen-like thing, etc.
For a general-purpose OS, the OS is assumed to have control of the CPU and can just use normal hardware protection. So it's primarily useful if you want to build an OS that can be installed inside an unprivileged user account on another OS. But in practice, most people grant their unprivileged user account enough privilege to use hardware-assisted virtualization.
Wrong. What Russell/Gödel/Turing/Rice/etc. tell you you can't do is write a decision procedure that checks arbitrary nontrivial properties of programs. In other words, if you first write a program and only then ask whether it is correct, you've already lost.
Obviously, the solution is to stop writing arbitrary programs. As Dijkstra said long ago, we need to find a class of intellectually manageable programs - programs that lend themselves to being analyzed and understood. Intuitively, this is exactly what programmers demand when they ask for “simplicity”. The problem is that most programmers' view of “simplicity” is distorted by their preference for operational reasoning, eschewing more effective and efficient methods for reasoning about programs at scale.
> Obviously, the solution is to stop writing arbitrary programs. As Dijkstra said long ago, we need to find a class of intellectually manageable programs - programs that lend themselves to being analyzed and understood.
You're overlooking the issue of self-reference. A given computer language can validate (i.e. prove correct) a subset of itself, but it cannot be relied on to validate itself. A larger, more complex computer language, created to address the above problem, can check the validity of the above smaller language, but not itself, ad infinitum. It's really not that complicated, and the Halting Problem is more fundamental than this entire discussion seems able to acknowledge.
Correctness is always relative to a specification. More precisely, it's the program's specification, which must exist prior to the program itself, which defines what it constitutes for the program to be correct. So a program that “validates itself” simply doesn't make sense.
Also, it seems you misunderstand Gödel/Turing/etc.'s result. What a consistent and sufficiently powerful formal system can't do is prove its own consistency as a theorem. Obviously, it isn't sustainable to spend all our time inventing ever more powerful formal systems just to prove the preceding ones consistent. At some point you need to assume something. This is precisely the rôle of the foundations of mathematics (or perhaps I should say a foundation, because there exist many competing ones): to provide a system whose consistency need not be questioned, and on top of which the rest of mathematics can be built.
In any case, we have gone too far away from original point, which is that, if arbitrary programs are too unwieldy to be analyzed, the only way we can hope to ever understand our programs is to limit the class of programs we can write. And this is precisely what (sound) type systems, as well as other program analyses, do. Undoubtedly, some dynamically safe programs will be excluded, e.g., most type systems will reject `if 2 + 2 == 4 then "hello" else 5` as an expression of type `String`. But, in exchange, accepted programs are free by construction of any misbehaviors the type system's type safety theorem rules out. The real question is: how do we design type systems that have useful type safety theorems...?
> So a program that “validates itself” simply doesn't make sense.
The language comes from Gödel's incompleteness theorems, in which there exist true statements that cannot be proven true, i.e. validated.
A given non-trivial computer program can be relied on to produce results consistent with its definition (its specification), but this cannot be proven in all cases.
It's not very complicated.
> This is precisely the rôle of the foundations of mathematics (or perhaps I should say a foundation, because there exist many competing ones): to provide a system whose consistency need not be questioned, and on top of which the rest of mathematics can be built.
This is what Russell and Whitehead had in mind when they wrote their magnum opus "Principia Mathematica" in the early 20th century. Gödel proved that their program was flawed. Surely you knew this?
> Also, it seems you misunderstand Gödel/Turing/etc.'s result.
> A given non-trivial computer program can be relied on to produce results consistent with its definition (its specification), but this cannot be proven in all cases.
Provability is always relative to a formal system. The formal system you (should) use to prove a program correct (with respect to its specification) isn't the program itself.
> Gödel proved that their program was flawed. Surely you knew this?
Gödel didn't prove the futility of a foundations for mathematics. Far from it. What Gödel proved futile is the search for a positive answer to Hilbert's Entscheidunsproblem: There is no decision procedure that, given an arbitrary proposition (in some sensible formal system capable of expressing all of mathematics), returns `true` if it is a theorem (i.e., it has proof) or `false` if it is not.
If you want to lecture someone else on mathematical logic, I'd advise you to actually learn it yourself. I'm far from an expert in the topic, but at least this much I know.
> Gödel didn't prove the futility of a foundations for mathematics.
Your words, not mine, but Gödel did prove that a non-trivial logical system cannot be both complete and consistent. As Gödel phrased it, "Any consistent axiomatic system of mathematics will contain theorems which cannot be proven. If all the theorems of an axiomatic system can be proven then the system is inconsistent, and thus has theorems which can be proven both true and false."
Gödel's result don't address futility, but completeness. That's why his theorems have the name they do.
> The formal system you (should) use to prove a program correct (with respect to its specification) isn't the program itself.
This refers to the classic case of using a larger system to prove the consistency of a smaller one, but it suffers from the problem that the larger system inherits all the problems it resolves in the smaller one.
I'm sorry, but 'catnaroek is completely justified here. Multiple people have told you that you are simply factually wrong in your interpretation of the halting problem, and you are acting arrogant about it. If you tone back the arrogance a bit ("Surely you knew this?", "The misunderstanding is not mine") and concede that, potentially, it's not the case that everyone else is wrong and you're right, you might understand what your error is.
It's a very common mistake and is frequently mis-taught, especially by teachers who are unfamiliar with fields of research that actually care about the implications of the halting problem and of Gödel's theorems (both in computer science and in mathematics) and just know it as a curiosity. So I've been very patient about this. But as I pointed out to you in another comment, you are misreading what these things say in a way that should be very obvious once you state in formal terms what it is that you're claiming, and it would be worth you trying to acknowledge this.
My original objection was to the claim that a non-trivial program could be demonstrated to be "provably correct." This statement is false. For non-trivial programs, it contradicts the simplest and most easily accessible interpretation of the Turing Halting problem and Gödel's incompleteness theorems, both of which demonstrate that this is not possible.
Quote: "Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist." (emphasis added)
> Multiple people have told you that you are simply factually wrong ...
So as the number of people who object increases, the chances that I am wrong also increases? This is an argumentum ad populum, a logical error, and it is not how science works. Imagine being a scientist, someone for whom authority means nothing, and evidence means everything.
In your next post, rise to the occasion and post evidence (as I have done) instead of opinion, or don't post.
> Quote: "Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist."
Do you agree or disagree that the quantifiers in these two statements are different? Do you agree or disagree that "the Turing Halting problem demonstrates that one cannot establish that every single non-trivial program is either 'provably correct' or 'provably incorrect'" is a different claim than the one originally made?
> My original objection was to the claim that a non-trivial program could be demonstrated to be "provably correct." This statement is false. For non-trivial programs, it contradicts the simplest and most easily accessible interpretation of the Turing Halting problem and Gödel's incompleteness theorems, both of which demonstrate that this is not possible.
You don't need to solve the Halting problem (or find a way around Rice's theorem, etc.) to write a single correct program and prove it so. A-whole-nother story is if you want a decision procedure for whether an arbitrary program in a Turing-complete language satisfies an arbitrary specification. Such a decision procedure would be nice to have, alas, provably cannot possibly exist.
To give an analogy, consider these two apparently contradictory facts:
(0) Real number [assuming a representation that supports the usual arithmetic operations] equality is only semidecidable: There is a procedure that, given two arbitrary reals, loops forever if they are equal, but halts if they aren't. You can't do better than this.
(1) You can easily tell that the real numbers 1+3 and 2+2 are equal. [You can, right?]
The “contradiction” is resolved by noting that the given reals 1+3 and 2+2 aren't arbitrary, but were chosen to be equal right from the beginning, obviating the need to use the aforementioned procedure.
The way around the Halting problem is very similar: Don't write arbitrary programs. Rather, design your programs right from the beginning so that you can prove whatever you need to prove about them. Typically, this is only possible if the program and the proof are developed together, rather than the latter after the former.
This much math you need to know if you want to lecture others on the Internet. :-p
> The way around the Halting problem is very similar: Don't write arbitrary programs. Rather, design your programs right from the beginning so that you can prove whatever you need to prove about them.
The system you outline works perfectly as long as you limit yourself to provable assertions. But Gödel's theorems have led to examples of unprovable assertions, thus moving beyond the hypothetical into a realm that might collide with future algorithms, likely to be much more complex than typical modern algorithms, including some that may mistakenly be believed to be proven correct.
If we're balancing a bank's accounts, I think we're safe. In the future, when we start modeling the human brain's activities in code, this topic will likely seem less trivial, and the task of avoiding "arbitrary programs," and undecidable assertions (or even recognizing them in all cases), won't seem so easy.
> This much math you need to know if you want to lecture others on the Internet.
My original objection was completely appropriate to its context.
> The system you outline works perfectly as long as you limit yourself to provable assertions.
Of course. And if a formal system doesn't let you prove the theorems you want, you would just switch formal systems.
> But Gödel's theorems have led to examples of unprovable assertions, thus moving beyond the hypothetical into a realm that might collide with future algorithms likely to be much more complex than typical modern algorithms, including some that may mistakenly be believed to be proven correct.
Programming is applied logic, not religion. And a proof doesn't need to be “believed”, it just has to abide by the rules of a formal system. In some formal systems, like intensional type theory, verifying this is a matter of performing a syntactic check.
> If we're balancing a bank's accounts, I think we're safe.
I wouldn't be so sure.
> In the future, when we start modeling the human brain's activities in code, this topic will likely seem less trivial,
I see this as more of a problem for specification writers than programmers. Since I don't find myself writing specifications so often, this is basically Not My Problem (tm). Even if I wrote specifications for a living, I'm not dishonest or delusional enough to charge clients for doing something I actually can't do, like specifying a program that claims to be an accurate model of the human brain.
> and the task of avoiding "arbitrary programs," and undecidable assertions (or even recognizing them in all cases), won't seem so easy.
I don't see what's so hard about sticking to program structures (e.g., structural recursion) for which convenient proof principles exist (e.g., structural induction).
Please, get yourself a little bit of mathematical education before posting your next reply. You're so stubbornly wrong it's painful to see.
> If we're balancing a bank's accounts, I think we're safe.
You seem to be contradicting your original claim, that it is impossible to prove any non-trivial program correct. Is this because you believe the program to balance a bank's accounts is trivial? Do you also believe that a C compiler is trivial?
I guess we never defined what you meant by "non-trivial." If your position is that the vast majority of software in the world today is "trivial," sure, I'd agree with you. But that's not really a meaning of "trivial" that anyone expected.
> "Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist."
You seem to be mixing up where the "for all" lies. The result is:
There does not exist a procedure that, for all (program, input) pairs, the procedure will say whether the program halts for that input.
{p | Ɐ(f,i): p(f,i) says whether f(i) will halt } = ∅
You are using it as if it said:
For all (program, input) pairs, there does not exist a procedure that will say whether the program halts for that input.
Ɐ(f,i): {p | p(f,i) says whether f(i) will halt } = ∅
"post evidence (as I have done)"
What is at issue is your incorrect assertions about what your evidence says. We read it, it contradicts you, everyone points this out, and you just ignore it and get louder.
> You seem to be mixing up where the "for all" lies.
Not at all. My original objection was to the claim that a program could be proven correct, without any qualifiers. Any program, not all programs. As stated, it's a false claim.
Your detailed comparison doesn't apply to my objection, which is to an unqualified claim.
> everyone points this out ...
Again, this is a logical error. Science is not a popularity contest, and in this specific context, straw polls resolve nothing.
> you just ignore it and get louder.
I wonder if you know how to have a discussion like this, in which there are only ideas, no personalities, and no place for ad hominem arguments?
(∃p ∈ P s.t. ¬(p ⊢ p ∈ C(halts)) ∧ ¬(p ⊢ p ∉ C(halts))) → ((p,s ⊢ p ∈ C(s)) → p is trivial)
Please supply a proof.
Note that it's quite true that
(∃p ∈ P s.t. ¬(p ⊢ p ∈ C(halts)) ∧ ¬(p ⊢ p ∉ C(halts))) → ((p,s ⊢ p ∈ C(s)) → *s* is trivial)
proved usually by reducing s to "halts" for any non-trivial s.
> Again, this is a logical error. Science is not a popularity contest, and in this specific context, straw polls resolve nothing.
I am not deciding it by poll. I am pointing out that there are objections to your reasoning that you have not addressed and persist in not addressing - despite them being made abundantly clear, repeatedly.
> I wonder if you know how to have a discussion like this, in which there are only ideas, no personalities, and no place for ad hominem arguments?
You're accusing me, as a person, of not understanding that a discussion like this has no place for accusations against a person? My complaint was not about you as a person, but about the form of your arguments in this discussion.
Can you clarify your last sentence? What do you mean by "preference for operational reasoning"? What's an example of the more effective methods for reasoning about programs at scale that you're contrasting this to?
“Operational reasoning” means using execution traces (the sequence of states underwent by a process under the control of your program) to derive conclusions about the program. You can do it in your head, using a piece of paper, using a debugger, using strategic assertions, etc.
By “more effective methods for reasoning about programs at scale”, what I mean is analyzing the program in its own right, without reference to specific execution traces. There are several kinds of program analyses that can be performed without running the program, but, to the best of my knowledge, all of them are ultimately some form of applied logic.
It's a guess, but I think GP uses "operational" as a synonym for "imperative". I think I encountered the term "operational semantics" in the context of Prolog programming. Denotational semantics is a term for a kind of semantics which are mathematically pure. IIRC Prolog has both operational and denotational semantics defined and they conflict. There's something about cut operator and tree pruning, but I read this long ago :-)
> It's a guess, but I think GP uses "operational" as a synonym for "imperative".
Not really. It's also possible to reason non-operationally about imperative programs, e.g., using predicate transformer semantics. It's also possible to reason operationally about non-imperative programs.
The Halting Problem helps us prove programs because it informs us that some functions cannot be computed. This means that the requirement spec for some computations cannot be implemented. When we spot this problem in a requirement spec, we instantly know that its proposed implementation is an incorrect program, no matter what that program is. We don't have to look at a single line of code.
But the halting problem for a subset of programs isn't The Halting Problem, which is the question whether a UTM can exist to calculate any function, over its entire domain.
The parent's wording was a little sloppy, but the point was that the grandparent was incorrectly using the Halting Problem to argue that you can't even do it for a meaningful subset of programs, which of course does not follow.
Here is something else: provably correct code can demonstrate unacceptable complexity for some input cases. We know from the proof that it will halt and the result will be correct: in 200 years on the given hardware. You have to add a time bound as a requirement specification to avoid this, or a constraint on the complexity (e.g. "the implementation must use no algorithm slower than quadratic time in such and such inputs").
How many modern programmers hold this mistaken belief? It's false -- the Turing Halting problem (https://en.wikipedia.org/wiki/Halting_problem) demonstrates that one cannot establish that a non-trivial program is "provably correct."
It seems the OP got carried away with his rhetoric, and the way he put it is simply wrong.