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

On Apr 30, 7:02 pm, "Paulo J. Matos" <pocma... at gmail.com> wrote:
>
> > I do not see the sense in going straight to an
> > implementation language (like the one that begins with a J) for such
> > systems. Well ok people may say performance, or the ability to recruit
> > staff, but I argue that  it would still seem worth creating an
> > executable in a language capable of expressing similar formalisms  as
> > an  oracle for testing your final implementation.
>
> I don't really understand what you mean here. If you mean that it is
> worth creating a model of your program using a formal method even if
> it doesn't allow you to create an executable program and then create
> the program separatly, then it suffers from a major problem.

No I meant the scenario where a formal specification already exists.

> It might
> be true that by writing the model you achieve a lot more understand
> about what you want to finally write but if you have a correct model
> of your program, and then you implement it independently, you can't
> make any kind of assertion by its correctness since you might have
> introduced errors during the translation.
>

Is the availability of an executable formal specification the
exception or the rule?

Regardless an executable specification may not be suitable for
deployment for reasons
stated in the original post, so some translation may be inevitable.

The primary scenario I have in mind is what to do when there is no
executable specification.