Formal specifications of programming languages

Formal specifications of programming languages

[Andrej Bauer]

I see people have opinions about formal semantics.

Having formal semantics for a programming language is a valuable thing,
even if most people do not understand it. Such semantics is a piece of
mathematics that removes (hopefully) every doubt as to what we are
talking about, and has other benefits as well. High priests can then
write sermons in common language and explain the meaning of the Holy Word.

It would probably be quite hard to provide formal semantics for complete
ocaml, for several reasons, such as sheer size, C interface, and the
fact that it is a moving target.

But what is formal semantics good for?

Complete formal semantics written with a tool such as Coq, together with
formal proofs of its properties (existence of principal types,
uniqueness of typing, type preservation, progress lemma) is good for
automatic extraction of a prototype type-checker and/or interpreter.
This can be extremely valuable for PL researchers who want to experiment
with new features.

Incomplete formal semantics written in a series of papers and
dissertations is still quite useful. It allows researchers to clearly
express and communicate ideas. Once a person learns how to read the
mathematics that may greatly help his or her understanding of corner
cases and peculiar examples.

We (researchers) should encourage "ordinary programmers" to read formal
semantics by writing manuals and textbooks that incorporate the
formalism and decorate it with sufficient explanation.

Think about the fact that specifying concrete syntax in BNF-like
formalism has become the norm. Programmers happily read it and the
benefits are obvious. Nobody suggests that syntax should be explained in
English prose because BNF is too hard to understand. So why are you
suggesting that the norm for describing other pieces of a programming
language, such as typing rules and operational semantics, should be
primarily (or only) English prose?

Andrej

Re: [Caml-list] Formal specifications of programming languages

[Christopher L Conway]

But, Andrej, we don't even have an *informal* semantics. :-( You've
got to walk before you run.

Chris

On Feb 13, 2008 1:22 PM, Andrej Bauer <Andrej.Bauer@fmf.uni-lj.si> wrote:
> I see people have opinions about formal semantics.
>
> Having formal semantics for a programming language is a valuable thing,
> even if most people do not understand it. Such semantics is a piece of
> mathematics that removes (hopefully) every doubt as to what we are
> talking about, and has other benefits as well. High priests can then
> write sermons in common language and explain the meaning of the Holy Word.
>
> It would probably be quite hard to provide formal semantics for complete
> ocaml, for several reasons, such as sheer size, C interface, and the
> fact that it is a moving target.
>
> But what is formal semantics good for?
>
> Complete formal semantics written with a tool such as Coq, together with
> formal proofs of its properties (existence of principal types,
> uniqueness of typing, type preservation, progress lemma) is good for
> automatic extraction of a prototype type-checker and/or interpreter.
> This can be extremely valuable for PL researchers who want to experiment
> with new features.
>
> Incomplete formal semantics written in a series of papers and
> dissertations is still quite useful. It allows researchers to clearly
> express and communicate ideas. Once a person learns how to read the
> mathematics that may greatly help his or her understanding of corner
> cases and peculiar examples.
>
> We (researchers) should encourage "ordinary programmers" to read formal
> semantics by writing manuals and textbooks that incorporate the
> formalism and decorate it with sufficient explanation.
>
> Think about the fact that specifying concrete syntax in BNF-like
> formalism has become the norm. Programmers happily read it and the
> benefits are obvious. Nobody suggests that syntax should be explained in
> English prose because BNF is too hard to understand. So why are you
> suggesting that the norm for describing other pieces of a programming
> language, such as typing rules and operational semantics, should be
> primarily (or only) English prose?
>
> Andrej
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

Re: [Caml-list] Formal specifications of programming languages

[Andrej Bauer]

Christopher L Conway wrote:
> But, Andrej, we don't even have an *informal* semantics. :-( You've
> got to walk before you run.

Didn't Jacques say in a related post "Most of the type system is
formalized, but there is no single place to look at"? Jacques, does the
"type system" mean "type checking", "type inference", "operational
semantics", or what. Heck, I should just look up the papers.

Maybe we should collect the relevant URLs and place them in the wiki. It
would be a start. I might do that.

Andrej

Re: [Caml-list] Formal specifications of programming languages

[Jacques Garrigue]

From: Andrej Bauer <Andrej.Bauer@fmf.uni-lj.si>
> Christopher L Conway wrote:
> > But, Andrej, we don't even have an *informal* semantics. :-( You've
> > got to walk before you run.
> 
> Didn't Jacques say in a related post "Most of the type system is
> formalized, but there is no single place to look at"? Jacques, does the
> "type system" mean "type checking", "type inference", "operational
> semantics", or what. Heck, I should just look up the papers.

This is mostly about providing a formal type system (what you would
call type checking) and prove that it admits principal types (so that
an inference algorithm exists). Of course, for the modules system
there is no inference (it still use core-language inference).

Concerning the operational semantics, the reference manual is quite
complete I believe. Of course some things are left unspecified, but
this is actually part of the specification (you should be able to
write programs without knowing the exact evaluation orer for instance.)
 
> Maybe we should collect the relevant URLs and place them in the wiki. It
> would be a start. I might do that.

Good idea indeed.

Jacques Garrigue

Re: [Caml-list] Formal specifications of programming languages

[Xavier Leroy]

> Didn't Jacques say in a related post "Most of the type system is
> formalized, but there is no single place to look at"? Jacques, does the
> "type system" mean "type checking", "type inference", "operational
> semantics", or what. Heck, I should just look up the papers.
>
> Maybe we should collect the relevant URLs and place them in the wiki. It
> would be a start. I might do that.

It's been done a long time ago: http://caml.inria.fr/about/papers.en.html

- Xavier Leroy

Re: [Caml-list] Formal specifications of programming languages

[Christopher L Conway]

Xavier,

Do any of these papers address existentials?

Regards,
Chris

On Thu, Feb 14, 2008 at 4:08 AM, Xavier Leroy <Xavier.Leroy@inria.fr> wrote:
> > Didn't Jacques say in a related post "Most of the type system is
>  > formalized, but there is no single place to look at"? Jacques, does the
>  > "type system" mean "type checking", "type inference", "operational
>  > semantics", or what. Heck, I should just look up the papers.
>  >
>  > Maybe we should collect the relevant URLs and place them in the wiki. It
>  > would be a start. I might do that.
>
>  It's been done a long time ago: http://caml.inria.fr/about/papers.en.html
>
>  - Xavier Leroy
>
>
>
>  _______________________________________________
>  Caml-list mailing list. Subscription management:
>  http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
>  Archives: http://caml.inria.fr
>  Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>  Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

Re: [Caml-list] Formal specifications of programming languages

[Jacques Garrigue]

From: "Christopher L Conway" <cconway@cs.nyu.edu>

> Do any of these papers address existentials?

There are no existentials in ocaml, only first-class universal types
(in polymorphic methods and polymorphic record fields.)
Universal types can be used to encode existentials through the usual
dual encoding.
The theory behind polymorpic methods is described in my paper with
Didier Remy, in the Objects section. Polymorphic fields in records are
simpler, and they were already formalized in earlier papers by Didier
Remy.

(Actually, abstract types in modules can also be seen as existentials,
but I don't think this is what you are talking about.)

Jacques Garrigue

Re: [Caml-list] Formal specifications of programming languages

[Jacques Carette]

Jacques Garrigue wrote:
> (Actually, abstract types in modules can also be seen as existentials,
> but I don't think this is what you are talking about.)
>   
This is a subtle issue that I have yet to understand 'completely'.  Can 
you expand on this "can also be seen as existentials" please?

To me, there seems to be a difference between these, but I have never 
been able to quite put my finger on it.  It may be because they are not 
really different, ie both can encode the other. 

This is not just an idle question.  In two separate papers (with 
co-authors), abstract types in module types (and Functors) are used as 
what I think of as "constrained existentials", to good effect.  But 
maybe I really ought to think of those as "for all types that can be 
used as implementations of this signature" rather than "some _specific_ 
type that satisfies this signature".  I say 'specific' because while 
users of the module cannot see the implementation, inside the 
implementation, the actual representation is rather crucial.

Jacques Carette

Re: [Caml-list] Formal specifications of programming languages

[Christophe Raffalli]

Jacques Carette a écrit :
> Jacques Garrigue wrote:
>> (Actually, abstract types in modules can also be seen as existentials,
>> but I don't think this is what you are talking about.)
>>   
> This is a subtle issue that I have yet to understand 'completely'.  
> Can you expand on this "can also be seen as existentials" please?
>
> To me, there seems to be a difference between these, but I have never 
> been able to quite put my finger on it.  It may be because they are 
> not really different, ie both can encode the other.
> This is not just an idle question.  In two separate papers (with 
> co-authors), abstract types in module types (and Functors) are used as 
> what I think of as "constrained existentials", to good effect.  But 
> maybe I really ought to think of those as "for all types that can be 
> used as implementations of this signature" rather than "some 
> _specific_ type that satisfies this signature".  I say 'specific' 
> because while users of the module cannot see the implementation, 
> inside the implementation, the actual representation is rather crucial.
Abstract types are existential types with a projecton operator (like a 
choice operator) and they can have contraints. Unfortunatly, modules are 
not first class and you can not do a list of modules with the same 
signature but distinct implementation for their abstract types. This is 
the lack of first class modules that prevent to encode existential types 
using abstract types.

The best to do is to use universal types in records with "the usual dual 
encoding" as said by J. Garrigues.

Do not forget that an abstract type occurring in the signature of an 
argument to a functor is a universal type because it is "negated" ...

>
> Jacques Carette
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs