Re: Nondeterminism (was: Formal semantics for C)

To: Viktor Kuncak <vkuncak@mit.edu>
Subject: Re: Nondeterminism (was: Formal semantics for C)
From: Fergus Henderson <fjh@cs.mu.oz.au>
Date: Thu, 27 Dec 2001 23:17:34 +1100
Cc: types@cis.upenn.edu
In-Reply-To: <200112270341.fBR3fbL18402@saul.cis.upenn.edu>; from vkuncak@mit.edu on Tue, Dec 25, 2001 at 12:00:11PM -0500
References: <200112221456.fBMEunr29447@saul.cis.upenn.edu> <200112221624.fBMGOdq04891@saul.cis.upenn.edu> <200112231526.fBNFQbM08076@saul.cis.upenn.edu> <200112251446.fBPEk5Q19557@saul.cis.upenn.edu> <200112270341.fBR3fbL18402@saul.cis.upenn.edu>
User-Agent: Mutt/1.2.5i

On 25-Dec-2001, Viktor Kuncak <vkuncak@mit.edu> wrote:
> It also seems to me that nondeterminism allows us to use
> languages with side effects without fixing an evaluation
> model.  I have impression that functional languages try to
> avoid such nondeterminism.  Is this because it is general
> hard to reason about such semantics?

Yes.

> Having nondeterminism is nice because it gives us more flexibility in
> program refinement.

Yes.  It's a trade-off.  More nondeterminism gives the compiler more
freedom to optimize the program, but can make it harder for programmers
to reason about their code.

Different languages allow differing amounts of nondeterminism,
depending on how the language designers weighed up this trade-off.

-- 
Fergus Henderson <fjh@cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.