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

On Thu, Apr 30, 2009 at 6:39 PM, wooks <wookiz at hotmail.com> wrote:
>
>
> On Apr 30, 7:02 pm, "Paulo J. Matos" <pocma... at gmail.com> wrote:
>> 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.
>>
>
> Putting  my question another way. If the languages have similar
> expressivity
> the potential risk of such errors is smaller. So to what extent is the
> expressivity similar.
>

By languages you mean programming languages and formal specification
languages? Well, I think they have quite different aims and I don't
think they have the same expressivity. Even if you could translate a
formal model into an executable, the resulting executable would
probably not be what you would expect it to be because the execution
model of a 'formal specification language'  is different from normal
execution models.

An example is Event-B. It is not executable in the sense that there is
no way to obtain an executable program from a specification (but on
the other hand, note that this is not important because Event-B focus
is in the formalisation of reactive systems, not software. Still, if
you try to model a sorting algorithm and translate the model into an
executable 'somehow' you would get a program that generates a random
array and sorts it just to go back to generating yet another array.

Again, I think if you want to focus on software verification B and
friends (B, Z, Event-B) are probably not the languages you would want
to have in your toolset (although some might disagree).

Sorry for the vague discussion but I am not sure how in-depth you want
an explanation to go. I can give you an example in the particular case
of B and friends if you are interested though.

However, I guess agda (as referenced before) would be something close
to a 'programming language for provably correct programs' if you know
what I mean.

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