Re: Point of formal semantics?

[John Clements <address@hidden>]

On Monday, June 2, 2003, at 06:14  PM, Horace Smith wrote:

> A formal semantics is invariably a mapping from one formal system to 
> another.
> E.g.
>
> logical language + inference rules -> sets and relations
> computer language + operations -> sets and relations
>
> Certainly proving that something gives you the same result in two 
> different formal systems might give you a little encouragement that 
> you're doing the right thing.
>
> But why does anyone claim that this gives you any clue as to the 
> "meaning" of the formal system on the left hand side?
>
> Why are some people so adamant that this sort of thing must be done?

Dictionaries specify the meanings of english words in terms of other 
english words.  Why does anyone claim that this gives you any clue as 
to the "meaning" of the words being defined?

In fact, a formal semantics isn't in nearly such dire straits, because 
we can use existing logical and mathematical frameworks (whose 
interpretation we tend to agree on) to specify the meanings of programs.

A formal semantics is the only way we have to precisely specify the 
result of evaluating a program written in that language.  The only 
difference between a formal and informal semantics is the degree of 
precision.  You could certainly write a "formal semantics" for a 
language in the language of prose rather than in the language of 
mathematics, but I think you'd find it unpleasantly verbose.

The process of writing a program is one of choosing a program 
(syntactic entity) whose meaning matches some internal model you have 
in your mind.  Without a formal semantics, you cannot be sure that 
these meanings match.

Finally and perhaps most significantly, casting a language's semantics 
in the language of logic and math allows us to use the proof tools 
associated with those frameworks to prove things about particular 
programs in a language, and often about *all* programs written in a 
language.  Type systems, for instance, typically seek to isolate a set 
of programs about which we can prove that certain kinds of errors don't 
occur.  In the absence of a formal semantics, it's hard to convince 
yourself (let alone others) that your type system "works".

One set of thoughts,

john clements