johnson@gregsun.nrtc.northrop.com (Greg Johnson <gjohnson>) (02/06/90)
In article <1990Jan25.173804.12259@tubsibr.uucp> hafer@tubsibr.uucp (Udo Hafermann) writes: >No, this is not a cross-posting. Nevertheless, the current discussion >about program verification in miscellaneous newsgroups prompts me to ask: > >1) Do you routinely prove your APL programs correct, i.e. convince > yourselves of the correctness by formal means? Do you write > Iverson-style identities? > This is a great question, one worthy of discussion. There are two levels at which one can talk about apl: the expressional sublanguage (the array manipulation operators, etc.) and the imperative sublanguage (goto's, etc.) The beauty of the language resides entirely in the first part; I think the latter part has little to recommend it. My feeling is that a given application area is appropriate for apl in direct proportion to the extent that it can be dealt with in the expressional sub-language. The expressional part of the language is not partial recursive (someone correct me here if I'm wrong; not sure about bizarre uses of `execute', or `modern' apls), so there are problems that cannot be solved with it. But this is no more indicting than to say that a scalpel cannot be used for all tasks, changing oil for instance. So, my comments are relevant only to the expressional part of the language. I am firmly convinced that apl encourages a style of thought that is conducive to proofs of program correctness. Dijkstra is known to rail at speakers if they let `operational thinking' creep into their understanding of programs; one should reason about programs in a way that is `outside of time;' i.e., one should not mentally execute the program to understand it and reason about it. Unfortunately, Dijkstra's programming languages and their associated program proof calculi fairly beg the programmer to think operationally. On the other hand, apl when used properly (i.e., when only the expressional part is used), mandates of the programmer that he think outside of time, apply Iverson-style identities, etc. If you are going to avoid apl loops (gag), and you want to write general programs (i.e. programs that operate on `arbitrary' inputs), you more or less have to think in a `program-proving', mathematical style. I think Backus's functional programming efforts can be understood as attempts to maintain the apl style of thought, but extend it to a partial recursive language. I think it would be interesting to combine apl and lambda calculus, i.e. recognize arrays as functions, and explore how to extend the apl array algebra to (in general, higher order) functions. If done right many of the Iverson apl identities might extend to this functional language, and one might gain a neat proof theory for lambda calculus-like languages. An interesting tie-in to the above is Alan Perlis's work with a colleague (whose name I forget) on extending apl arrays to infinite dimensions and writing an interpreter using lazy evaluation. At least in that language you can write a non-terminating expression, a prerequisite for partial recursiveness! - Greg Johnson