On 3/4/06, Eugene Salamin <gene_salamin@yahoo.com> wrote:
There appears to be a basic problem with automated program checking. You have to provide two inputs, the program to be checked, and a description of what the program is supposed to do. But this description will have to be constructed by error-prone humans, and so we still have the problem of verifying the correctness of the descripton. Indeed if the description language is less confusing and less prone to mistakes than the program language, the description language should supplant the program language. What better way is there to create a program, than to describe what you want, and let the computer do it for you.
Uh-huh --- here's my spec, then. [It's a little informal, but the details may be fleshed out a la Goedel in any way you please.] Given as input a self-contained program in (say) ALGOL68 [the only high-level programming language I have encountered to be defined in a convincingly precise, albeit utterly incomprehensible, fashion], compile a debugger which outputs true,false according to whether its input will terminate,loop infinitely resp. What this example demonstrates is that "programming languages" and "specification languages" are entirely different animals. [By the way, you can't wriggle out of it by outputting "can't be done!" instead of a piece of object code --- that problem is also undecidable!] Fred Lunnon