I've always felt that the real problem with automatic proof systems is proving that what is being proved (presumably a machine-understandable specification) is equivalent to what you actually want to prove (presumably a natural language description). Perhaps this is less of a problem for mathematical theorems than it is for programs? --ms On 3/18/2012 1:46 AM, Henry Baker wrote:
I've been told that Java (not Javascript) routinely "proves" that new modules can't overrun their boundaries when the modules are loaded.
I've also been told that Microsoft is routinely checking many/most of its device drivers to have certain properties. Microsoft is apparently a fan of "model checking", which is a certain restricted type of theorem proving.
I've also been told that there are several types of operating systems that have been proven "secure" -- whatever that means.
I've been told that Intel has routinely been checking their floating point implementations ever since the infamous Pentium bug incident.
The only thing holding "Wikiproofia" back right now is a small, dedicated "open source" project to focus on this for a good 5-10 years to develop the basic core system and a good library of "lemmas" to cover many of the more obvious things that need to be proven.
"Artificial Intelligence" isn't needed right this second; that would only be required if you didn't want to have to explain every last detail to the proof checker; but many of the details would already be handled by a large enough library of already proven lemmas.
At 07:47 PM 3/17/2012, Fred lunnon wrote:
On 3/18/12, Marc LeBrun<mlb@well.com> wrote:
="Henry Baker"<hbaker1@pipeline.com> mechanically _check_ submitted proofs I agree this is a good idea, but have wondered how far off the dream is. ... Is Wikiproofia's first customer release date inevitably post-singularity? There are certainly plenty of projects aimed in this direction --- just search on "automated theorem proving". But I think they're unrealistic, for much the same reasons Marc advanced.
If you can't solve the problem, look for an easier one instead. In this case, the easier problem is automatic verification that a computer program implements its specification. Here the universe is extremely circumscribed, and well documented. When we've got that question satisfactorily answered, then it might be time to look seriously at automated theorem proving.
I have a vague memory of some bigwig in the UK MoD --- or maybe it was the USA DoD --- announcing grandiosely in public that in future all defence contracts would include a clause demanding that any software be proved correct. That was some time in the 1970's. When we'd all stopped laughing, we said --- quietly, of course --- don't hold your breath!
But after all the ballyhoo has been deflated, and the journalists and politicians have departed to look for other mirages to chase, things do eventually come quietly to pass in a lab somewhere out of the spotlight.
In the end, Deep Blue defeated Kasparov ...
Fred Lunnon
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com http://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun