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

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.