Re^5: Comparative satisfiability of regexps.

In programming in particular, there's almost always a formal proof of correctness available.

I have to counter that statement.

Formal proof of a computer program's correctness is not possible. and anyone suggesting to you that it is, is not a scientist, but a snakeoil salesman.

Formal proof of an algorithm is possible.

And you can certify a particular implementation on a particular hardware setup--with the use of comprehensive and rigorous testing--provided the domain and range of every variable can be determined and catagorised. But it had best be a very important, and probably very simple program.

Any other kind of "proof" is either statistical or snakeoil.

Examine what is said, not who speaks.

Silence betokens consent.

Love the truth but pardon error.

Comment on Re^5: Comparative satisfiability of regexps.

Replies are listed 'Best First'.
Re^6: Comparative satisfiability of regexps. by Meowse (Beadle) on Jan 21, 2005 at 01:12 UTC
Indeed, I should have said, "In reasoning about formal logic, and algorithm design in particular, there's almost always a formal proof of correctness available." And even then, one must keep in mind Knuth's famous, "Be careful in using this algorithm. I have only proven it correct, not tested it." But statistical proof is, IMHO, no proof at all. It is at best evidence. Take care, Mickey.	[reply]