[Prev][Next][Index][Thread]
Re: comments on my course outline
Return-Path: <kfoury@bu-cs.bu.edu>
Date: Fri, 7 Oct 88 18:08:30 EDT
To: jcm%ra.stanford.edu@STORK.lcs.mit.edu, types@theory.LCS.MIT.EDU
Concerning what is appropriate for an introductory course
on Prog Lang Theory.
In response to John, yes, I am in favor of introducing Hoare
logic -- and this is what I do in my own course. I agree that
it is difficult to integrate it in a course whose starting point
is the lambda-calculus, e.g., the sequence of topics John chose
for his course. There is an unavoidable break between Hoare logic
stuff (the first part of my course) and lambda-calculus stuff (the
second part of my course). I don't try to put the two in a single
framework, which I don't believe to be a criterion for a good
introductory course. Michael Gordon takes this approach in his new
"Programming Language Theory" (Prentice-Hall, 1988) but I am not
entirely happy with his presentation and choice of topics:
(1) On Hoare logic, he discusses the fundamental issues of soundness
and completeness, but chooses "mechanizing program verification" rather
than relative completeness and some of the issues from Clarke's thesis.
(2) On the lambda-calculus, his presentation is entirely based on the
untyped (a mistake in my opinion) and some parts are more about
computability theory (e.g., representing the partial rec functions)
than about prog language theory (e.g., no discussion of semantics and
no mention of the fundamental distinction between operational and
denotational, parallelling the distinction proof-theory/model-theory).
Without really understanding what Matthias means by a "theory of
programming language expressiveness", I still wonder whether it can
be used to introduce students to the basic concepts necessary for ANY
further programming language theory. From what I can guess, prog lang
expressiveness is one kind of theory (no doubt interesting), but
I believe students should be exposed to several of the fundamentals
first. Perhaps we first have to agree what are these fundamentals for
prog lang theory.
Dennis