```
Subject:
```**Re: PLOT: A non-parenthesized, infix Lisp!**

From: rpw3@rpw3.org (Rob Warnock)

Date: Sat, 02 May 2009 20:41:51 -0500

Newsgroups: comp.lang.lisp,comp.lang.misc,comp.lang.scheme

Message-ID: <q7adnU5Bm_7Ca2HUnZ2dnUVZ_qWdnZ2d@speakeasy.net>

Scott Burson <FSet.SLB@gmail.com> wrote: +--------------- | Halting Problem says that termination is uncomputable: that there is | no algorithm that can tell you, for every program P, whether P | terminates. Yet proofs of termination of particular algorithms are a | staple of CS work. So if the specification of a program includes the | statement that the program terminates -- which is certainly a well- | defined property -- then proving that the program meets that aspect of | the specification, while clearly possible in almost all cases of | interest, is uncomputable. So there is _some_ formal method of | proving that the program has this property; it's just not a method | that we know how to automate (well enough to be generally useful). +--------------- The situation is neither as dire *nor* as favorable as many who argue the extremes may wish to portray. If you're given a random program and asked to prove whether or not it conforms to some other random specification -- even as simple as "it terminates" -- then, yes, this is uncomputable *in general*. However, individual program instances *might* be provable. You just don't know which ones until you try [and your proof system either terminates... or doesn't]. The real problem, IMHO, is that we have all [well, mostly all] been ignoring the advice of people like Dijkstra & Gries &c. who recommend abandoning the whole "try to prove that program A meets spec B" approach, and instead suggest growing the program *and* the proof *together* from the spec, using "predicate transformers" to work backwards in a formal, provable manner from the desired results [the "post-conditions"] to the specified initial conditions [the "pre-conditions"]. There is no issue of computability with the approach, since at no time is the program that's being constructed allowed to contain unprovable elements. Dijkstra's famous monograph on this approach is called "A Discipline of Programming": http://www.amazon.com/dp/013215871X Gries's later textbook, which might be more approachable to many, is called "The Science of Programming": http://www.springer.com/computer/programming/book/978-0-387-96480-5 http://www.amazon.com/dp/0387964800 But to bring my diversion back on-topic, the theoretical problem with the Dijkstra/Gries approach is that the technique is not constructive, and hence cannot be (fully) automated. Specifically, proving loop termination involve searching for a loop invariant predicate that meets the pre- & post-conditions [less the termination condition] *and* "makes non-zero progress" [typically decrements a positive number, where said number being zero is the termination condition]. Once you have found some appropriate loop invariant predicate, the proof of correctness and termination of the loop is trivial [and is trivially automatable]. Unfortunately, their formal method doesn't help you at all in *finding* such a predicate!! All one has available for guidance is "style", "experience", "heuristic", etc. [One is reminded of Shannon's famous Coding Theorem, which proves that, given some specific channel, a block code exists that can produce throughput "as close as you like" to the theoretical maximum information carrying capacity of the channel with, at the same time, an error rate "as low as you like"... but does not provide *any* guidance as to how to *find* such a block code!! (*sigh*)] Still, I suspect that creating an "expert system programming assistant" to help programmers find appropriate loop invariant predicates using Dijkstra's formalism would, in the long run, be a more effective use of resources than continuing to beat our heads against the *known* incomputable wall of "write it first *then* try to prove it". -Rob ----- Rob Warnock <rpw3@rpw3.org> 627 26th Avenue <URL:http://rpw3.org/> San Mateo, CA 94403 (650)572-2607