|
![](/i/fill.gif) |
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
|
![](/i/fill.gif) |