Darren New wrote:
> Orchid XP v8 wrote:
>> Isn't trying to figure out why an arbitrary piece of code doesn't work 
>> formally equivilent to the Halting Problem? 
> 
> No.
> 
> The code works, in the formal sense. It just doesn't do what you want it 
> to do.

Or, to clarify...

If by "works" you mean "obeys the formal specification", then yes, you can 
prove it.  Write a formal spec for what sequence a Haskell program can 
output, such as a BNF grammar. Now analyze your Haskell program to see if 
the parser you wrote follows the BNF.

Computers do this all the time. There's an input language the compiler 
accepts. It can tell whether the input matches the language spec, and if so, 
the program "works", in some sense.

And indeed, this is called the field of "program verification", pioneered by 
those who invented structured programming and such.

-- 
Darren New, San Diego CA, USA (PST)
   Linux: Now bringing the quality and usability of
   open source desktop apps to your personal electronics.

Post a reply to this message