Neohapsis is currently accepting applications for employment. For more information, please visit our website www.neohapsis.com or email firstname.lastname@example.org
From: Michael Wojcik (Michael.Wojcikmerant.com)
Date: Fri Jul 06 2001 - 09:01:54 CDT
A quick (and arguably on-topic) note about program proofs: interested
readers might want to check out Philip Wadler's article on logic systems and
programming languages, "New Languages, Old Logic", from the _Dr Dobb's
Journal_ special issue on "Programming in the 21st Century". It
discusses automated theorem and program proving, including some real-life
examples of automated program proving for production software.
While program proofs are impossible in the general case (Halting), and
impractical in most cases (at least with the current state of the art),
there are limited domains where they're in use.
Michael Wojcik michael.wojcikmerant.com
Department of English, Miami University