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

On Thu, Apr 30, 2009 at 5:37 PM, wooks <wookiz at hotmail.com> wrote:
> To what extent can a programming language (of the right type)
> replicate the expressivity of formal languages.
>

What do you mean by formal languages?

> It seems to me that if an organisation is going to deploy formal
> methods  then it would always make sense to do an implementation in a
> language that as far as possible retains the same expressive
> constructs.

True, the B-Method achieves this by allowing the developer to define
the model in layers, where the layer below is a refinement of the
layer above (which include more 'detail'). By including more detail in
each layer you end up with a language called B_0 that can be compiled
(or easily converted to a programming language automatically). Along
the way for each layer you need to prove all the invariants and for
each layer transition you need to prove gluing invariants.

> 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. 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.

>
> Second question. What is the difference between formal languages and
> modelling languages (is the answer the degree of formalism?).

Again, formal languages is a bit of an awkward concept I guess and
different people might have different answers for that.

Anyway, one interesting path for software development (which I haven't
looked in detail yet) is agda:
http://wiki.portal.chalmers.se/agda/agda.php?n=Main.HomePage

Cheers,

Paulo Matos

> _________________________________________________
>  For list-related administrative tasks:
>  http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>



-- 
Paulo Jorge Matos - pocmatos at gmail.com
Webpage: http://www.personal.soton.ac.uk/pocm