Newsgroups: comp.lang.misc
Path: utzoo!utgpu!watserv1!watmath!tolstoy.waterloo.edu!mhcoffin
From: mhcoffin@tolstoy.waterloo.edu (Michael Coffin)
Subject: Re: Formal definitions (Re: ada-c++ productivity)
Message-ID: <1991Apr16.154520.21362@watmath.waterloo.edu>
Sender: news@watmath.waterloo.edu (News Owner)
Organization: University of Waterloo
References: <1954@optima.cs.arizona.edu>
Date: Tue, 16 Apr 1991 15:45:20 GMT
Lines: 18

In article <1954@optima.cs.arizona.edu> David Gudeman writes:

>... If your specification is so great, why not make that your
>programming language?

Because the specification abstracts away details that are necessary
for producing efficient code but unnecessary for correctness.  The
specification for a program that sorts a file might be some formal
translation of "the output file consists of the same lines as the
input file, but in alphabetical order".  But as years of research and
tons of journal articles demonstrate, turning that specification into
an efficient program is not trivial---certainly not so trivial that a
compiler could accomplish it.

Michael Coffin				mhcoffin@watmsg.waterloo.edu
Dept. of Computer Science		office: (519) 885-1211
University of Waterloo			home:   (519) 725-5516
Waterloo, Ontario, Canada N2L 3G1