From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-0.8 required=5.0 tests=BAYES_00,INVALID_DATE,
	MSGID_SHORT autolearn=no autolearn_force=no version=3.4.4
Path: utzoo!utgpu!watmath!clyde!att!pacbell!ames!mailrus!cornell!rochester!pt.cs.cmu.edu!sei!dd
From: dd@sei.cmu.edu (Dennis Doubleday)
Newsgroups: comp.lang.ada
Subject: Re: Collective response to := messages
Message-ID: <7832@aw.sei.cmu.edu>
Date: 29 Nov 88 14:39:26 GMT
References: <8811282217.AA04896@ajpo.sei.cmu.edu>
Organization: Carnegie-Mellon University (Software Engineering Institute), Pgh, PA
In-reply-to: mendal@ANNA.STANFORD.EDU's message of 28 Nov 88 22:19:34 GMT
List-Id: <comp.lang.ada>


In article <8811282217.AA04896@ajpo.sei.cmu.edu> mendal@ANNA.STANFORD.EDU (Geoff Mendal) writes:
>But the point is that the current semantics of assignment do allow
>program provers to make certain assumptions which make the job of
>writing a program prover easier.  While it is certainly possible to
>write a program prover which does not make use of the current
>assignment semantics, it is far harder to do so.  The point being that
>there exist applications of Ada out there which will suffer somewhat
>from this proposed language change.  Whether this is a desired result
>is debatable (do we really want to force the program proving folks to
>go back and undertake a major redesign because a few programmers hate
>to type ASSIGN?).

I agree that overloading of ":=" is a bad idea, but your line of
reasoning here is not convincing (to me).  I would change your last
question to "are we really going to limit programmers to only those
language constructs which the program proving folks find easy to
handle?".  If the answer is "yes", then we're not going to get much
real work done for the next decade, at least.

Dennis Doubleday                       dd@sei.cmu.edu
Software Engineering Institute         (412)268-5873
Carnegie Mellon University
Pittsburgh, PA 15213