3 ms·

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

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

lutusp 11y ago
> 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. The misunderstanding is not mine.
- catnaroek 11y ago
  > 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.
  - lutusp 11y ago
    > 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. > If you want to lecture someone ... This is either beneath you, or it should be.
    - geofft 11y ago
      > This is either beneath you, or it should be. 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.

lutusp 11y ago

> 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. The misunderstanding is not mine.

catnaroek 11y ago
> 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.
- lutusp 11y ago
  > 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. > If you want to lecture someone ... This is either beneath you, or it should be.
  - geofft 11y ago
    > This is either beneath you, or it should be. 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.