Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!swrinde!elroy.jpl.nasa.gov!ncar!noao!arizona!gudeman
From: gudeman@cs.arizona.edu (David Gudeman)
Newsgroups: comp.lang.misc
Subject: Re: Proving correctness of programs in functional languages
Message-ID: <3154@optima.cs.arizona.edu>
Date: 14 May 91 06:12:49 GMT
Sender: news@cs.arizona.edu
Lines: 42

In article  <873@saxony.pa.reuter.COM> Dave Gillett writes:

]     This exercise is entirely in terms of functions and predicates,
]which are mathematical objects, and any well-defined functional
]notation is sufficient to allow us to proceed to proof.
]
]     By contrast, the majority of the literature that I have seen on
]the verification of procedural programs starts, instead, from the
]notion that a program is a "text".  Resolution of syntactic and
]semantic issues, in order to arrive at suitable objects for
]reasoning, becomes a major task; indeed, there is rarely time or
]space left for the actual proof itself.

This has nothing to do with the distinction between functional
languages and procedural languages.  You have to have a meaning
function from the text to the semantic domain for any kind of
language.  If functional-language proofs don't discuss this, then it
is just because the writers are being sloppy about the distinction
between syntax and semantics.  Actually though, all the semantics I
have seen for functional languages _do_ address these issues.

The syntactic issues of many procedural languages are complicated by
type declarations, maybe that is what you are thinking of.  But the
existence of type declarations is orthogonal to the mechanism of the
language (functions, procedures, or predicates).  You can have a
functional language with type declarations and a procedural language
without them.

The apparent semantic simplicity of functional languages is an
illusion created by the fact that the functional languages whose
semantics have been described are just simple languages.  I can define
a procedural language that parallels the lambda calculus.  It has the
same number of basic forms and the semantics is no more complex.

If you want to compare the "semantic simplicity" of different
paradigms you just can't compare Pascal to FP, nor Turing Machines to
the lambda calculus.  You have to compare languages with the same
expressiveness and the same limitations.
--
					David Gudeman
gudeman@cs.arizona.edu
noao!arizona!gudeman