[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Point of formal semantics?
On Monday, June 2, 2003, at 06:14 PM, Horace Smith wrote:
> A formal semantics is invariably a mapping from one formal system to
> 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,