[Prev][Next][Index][Thread]

Re: Nondeterminism / formal semantics of C

> As for whether the semantics should be _mathematical_, well, currently
> structured English ("Standardese") seems in most cases to be more useful
> than mathematics for language definitions and programming language
> standards, because it can be more easily understood by a wider audience.

this may be correct at the moment but there is an important audience which 
cannot understand structured english:  verification tools!
 
> But currently the state-of-the-art in tools for making use of formal
> semantics seems to be well behind that for grammars.  Until we have
> better tools, and these tools become widely used and widely accepted,
> the advantages of mathematical specifications will be limited.

this is incorrect. there is a mathematically totally rigorous, yet also
conceptually simple tool for semantic specifications: ad-hoc operational
semantics, SOS, labelled transition systems and the like. i cannot
think of a single example where the ad-hoc semantics wasn't leaner cleaner
in comparison with alternative semantic specifications, be they game-theoretic, 
pi-calculistic or functional (lambda calculi or domains). 

of course there is a  problem with ad-hoc operational semantics and that 
is that they

* don't allow (or facilitate) technology transfer. by that i mean that
  because of the lack of constraints on, say, rule formats, it is usually
  not possible to reuse technology such as theorem provers
  or control-flow analyses (developed for one ad-hoc semantical framework)
  in another, at least not without having to do conceptually trivial yet 
  nevertheless substantial reworking of proofs
 
* in addition and for the same reasons there isn't a widely applicable
  collections of reasoning methods for ad-hoc semantics.

nevertheless, the benefits (in precision) of ad-hoc semantics over informal 
methods are so substantial that the reasons for refusing to do formal 
specifications of programming languages can no longer be technical, just 
social.

BUT of course it would be nice if it was possible to identify a 
'universal' ad-hoc operational semantics that was

* expressive enough to allow precise and concise modelling of all
  computational phenomena, but was

* small and constrained enough so that we can finally start (and hopefully
  eventually succeed) to develop non-trivial and practically useful
  mathematical theories of computing (comparable to the role of differential
  equations in physics)

now the good news: such a universal ad-hoc semantics may already exist!
it is called the (asynchronous) pi-calculus. 

martin