[plt-scheme] Re: Expressivity gap between formal methods and PL's

On Thu, Apr 30, 2009 at 12:53:04PM -0700, wooks wrote:
> 
> 
> On Apr 30, 8:25 pm, "Paulo J. Matos" <pocma... at gmail.com> wrote:
> 
> >
> > What do you mean, what to do? If we are here thinking about formal
> > specification of software, then there really is nothing you can do.
> >
> 
> Well I want to go from having a (hopefully) correct formal spec of my
> system to
> a correctly functioning system.
> 
> >
> > You specify your model just to get a better understand of how it works
> > in a formal language and then you implement it in a programming
> > language trying to maintain invariants.
> >
> 
> If I had a formal specification of a system then I'd want to get alot
> more out of it.
> 
> So what are the sorts of things I can express in a formal
> specification language that
> do not readily translate to programming languages.
> 
> What sorts of things are the biggest threats to the fidelity of the
> translation.
> 
> Perhaps another way of looking at it is if you decided to implement
> (lets say Z in Scheme/Lisp)
> what constructs would be the most troublesome to implement.
> 

You could have operations such as "pick an arbitrary element of set S"
This could be really hard to implement depending on the specification of 
the set S (such as, for example, the set of all nonhalting Turing 
machines).

-- hendrik