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"[1]. 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.

[1] http://www.ddj.com/articles/2000/0013/0013g/0013g.htm

Michael Wojcik michael.wojcikmerant.com
MERANT
Department of English, Miami University

• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]