Re^4: Comparative satisfiability of regexps.

All true, and well-said, except that the precise commodity desired in this case is proof of the compatibility of two unprovable entities. My code neither knows nor cares what the two regexps "mean", or whether they correctly represent the author's intent; it only cares that output which satisfies the first regexp can be affirmatively stated to satisfy the second regexp.

In our particular instance, we're attempting to verify the correctness of a meta-application built of sequentially assembled functoids whose input and output contracts are specified as .xsd files. We don't want to know what any given functoid does, or what its parameters (or outputs) represent. We just want to verify that a given sequence of correct functoids is itself correct.

As a separate note, I'm really disinclined to accept Monte Carlo proofs in the hard sciences. I'll accept them in the soft sciences, but only because there aren't better alternatives. In programming in particular, there's almost always a formal proof of correctness available.

Thanks much,

Mickey.

Comment on Re^4: Comparative satisfiability of regexps.

Replies are listed 'Best First'.
Re^5: Comparative satisfiability of regexps. by BrowserUk (Patriarch) on Jan 20, 2005 at 16:09 UTC
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.	[reply]
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]
Re^5: Comparative satisfiability of regexps. by sleepingsquirrel (Chaplain) on Jan 20, 2005 at 23:04 UTC
As a separate note, I'm really disinclined to accept Monte Carlo proofs in the hard sciences. I guess that means you don't trust public key encryption then, because RSA needs prime numbers to work with, but everybody just uses a variation of the Fermat test to check whether the keys generated are probably prime. But most people aren't overly concerned by this because you can set your threshold for "probably" to be, say, 100 times lower than the probablity that cosmic radiation will flip a bit in your memory causing an otherwise perfect algorthim to fail. -- All code is 100% tested and functional unless otherwise noted.	[reply]
Re^6: Comparative satisfiability of regexps. by Meowse (Beadle) on Jan 21, 2005 at 01:10 UTC
I still maintain that there's a difference between quantifiable stochastic approaches (where one can state definitively how likely it is that the number is non-prime) and Monte Carlo approaches (where one throws possible disconfirming values at it until one "feels confident" that it's "tested enough"). If the nature of your regexps were such that you could say "of the possible million values in the range, we have tested a randomly selected 10% of them, and thus we are reasonably confident that the regexps will work for all values", I'd be willing to consider it as evidence, if not functional proof. But with a potentially infinite range for the regexps, I wouldn't even consider it evidence. Take care, Mickey.	[reply]
Re^6: Comparative satisfiability of regexps. by Aristotle (Chancellor) on Jan 21, 2005 at 12:20 UTC
That analogy is flawed. That's how public key cryptography is implemented in practice, for practical reasons, to be sure. It's not how the cryptographic algorithms are constructed mathematically, however. And of course there's the quantifiable vs Monte Carlo difference Meowse mentioned. Makeshifts last the longest.	[reply]