Lambda the Ultimate

inactiveTopic Why Donít Programming Language Designers Use Formal Methods?
started 8/24/2002; 2:49:11 AM - last post 8/27/2002; 3:44:48 AM
jon fernquest - Why Donít Programming Language Designers Use Formal Methods?  blueArrow
8/24/2002; 2:49:11 AM (reads: 2015, responses: 2)
Why Donít Programming Language Designers Use Formal Methods?
An argument for Action Semantics. Discusses the life cycles of some languages (Pascal , ADA-83, ML) and how they failed to use formal specifications until long after they'd actually been specified. Action Semantics emphasizes pragmatics and can specify the semantics of imperative, object-oriented, functional, and concurrent programming languages.

...these specifications are unusually writable, modifiable, reusable, and readable. These qualities are consequences of the design of action notation. Familiar programming language concepts like binding, storing, sequencing, iteration, etc., are directly expressed in action action-semantic specification reads rather like an operational specification expressed in English.

There is also an Action Semantics home page that has three well-written tutorials:

Also note that Action Semantics influenced Espinosa's Scheme monad-based Semantic Lego ("Why Donít Programming Language Designers Use Formal Methods?", David A. Watt, 1996)
Posted to implementation by jon fernquest on 8/24/02; 3:23:25 AM

jon fernquest - Re: Why Donít Programming Language Designers Use Formal Methods?  blueArrow
8/27/2002; 3:44:48 AM (reads: 884, responses: 0)
The semantic lego <-> action semantics connection:

Peter Mosses describes action semantics, a reformulation of his theory of ab- stract semantic algebras. Mosses attempts to achieve modularity in semantics by defining an intermediate level, called actions, into which one can translate language constructs. Actions are low-level enough to be flexible, but high-level enough to hide the details of interactions between facets of a language.

Since Mosses has not yet been able to combine facets, he gives a single algebra of actions, with environments, stores, etcetera. This algebra corresponds to a single stratified monad generated by the toolkit. Mosses's theory is more modular than pure denotational semantics because constructs are isolated from each other, but, from our point of view, it is not modular at all. One can only define modularly the constructs that the algebra was designed to define. That is, one can define stores modularly because the fixed algebra of actions includes modular stores.

Recalling that Moggi cites Mosses's comments on the non-modularity of denotational semantics, we can more gently view the toolkit as a final step in Mosses's program. Stratified monads could be the modular facets Mosses was looking for.

From: ("Building Interpreters by Transforming Stratified Monads", David Espinosa, 1994)

Can't find anything extending Espinosa's work. Is Espinosa's work a dead end or are people still interested in his ideas?