comment on

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.

In reply to Re^5: Comparative satisfiability of regexps. by BrowserUk
in thread Comparative satisfiability of regexps. by Meowse

Are you posting in the right place? Check out Where do I post X? to know for sure.
Posts may use any of the Perl Monks Approved HTML tags. Currently these include the following:
<code> <a> <b> <big> <blockquote> <br /> <dd> <dl> <dt> <em> <font> <h1> <h2> <h3> <h4> <h5> <h6> <hr /> <i> <li> <nbsp> <ol> <p> <small> <strike> <strong> <sub> <sup> <table> <td> <th> <tr> <tt> <u> <ul>
Snippets of code should be wrapped in <code> tags not <pre> tags. In fact, <pre> tags should generally be avoided. If they must be used, extreme care should be taken to ensure that their contents do not have long lines (<70 chars), in order to prevent horizontal scrolling (and possible janitor intervention).
Want more info? How to link or How to display code and escape characters are good places to start.


Problems? Is your data what you think it is?
	PerlMonks