5 ms·

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

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.

jonahx 11y ago
Nice post. 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?
- catnaroek 11y ago
  “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.
- klibertp 11y ago
  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 :-)
  - catnaroek 11y 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.
lutusp 11y ago
> 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.
- catnaroek 11y ago
  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.

jonahx 11y ago

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

catnaroek 11y ago
“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.
klibertp 11y ago
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 :-)
- catnaroek 11y 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.

lutusp 11y ago

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

catnaroek 11y ago
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.