Wednesday, September 05, 2007
Progress is what matters
It's a well-known slogan in PL theory circles that Type Soundness = Preservation + Progress. But sometimes, people just write the Preservation lemma. Sometimes they even confuse type soundness with type preservation. Richard and I were chatting today and he reminded me that the goal of a type soundness theorem is to guarantee the absence of runtime type errors. In that sense, just proving that expressions remain well-typed is skipping the punch-line. The Progress lemma tells you that, assuming you're well-typed, you'll never get stuck with a type error--that's the point!
Subscribe to:
Post Comments (Atom)
3 comments:
I think these people are just sloppy and informal, I doubt they confuse soundness with preservation. In my experience, preservation is a lot harder to prove and much more insightful than progress -- the preservation proof reveals very subtle bugs in your rules, whereas if progress fails, it's usually due to a really obvious mistake that you'd easily eyeball by just looking at the rules.
In short, preservation and progress are usually about the same length on paper but preservation holds the overwhelming majority of the information content in a soundness proof.
An even better-known slogan is
"Well-typed programs don't go
wrong". While it's not clear just
what "wrong" means, I'd suggest
that it includes getting stuck. So
if you keep that slogan in mind,
you'll be reminded of what you
have to prove.
By the way, whose character were
you assassinating with this post?
:-)
-- Paul
I see type preservation as a more important soundness lemma, in the sense that it is a technique to possibly prove several soundness theorems. Progress is one of the properties one might prove of a well-typed program, so that preservation + progress can prove that well-typed programs always progress. But in fact any property P implied immediately by well-typedness can be proved to be an invariant by preservation. In particular for safety properties, P can be any specification of "a counterexample to safety cannot be found immediately"; blocking is often considered safe, especially when P is intended to be a security invariant.
Post a Comment