Alex Cruise posted the link on the Scala language mailing list to these slides by Benjamin Pierce (along with Nate Foster and Michael Greenberg). Pierce is the author of Types and Programming Languages (which I confess I'm still working my way through).
Even if you have absolutely no interest in type systems, these slides are worth a look for their punchy visuals. Perhaps Pierce should also teach a course on the effective use of PowerPoint.
What Pierce is getting at (if I understand right) is that type systems can get too heavyweight to be worth the trouble. He's looking at a particularly complex case, that of the Boomerang programming language, so perhaps the typechecking in your favorite language (if it's not Boomerang) may still be lightweight enough not to be under suspicion.
Pierce's conclusion seems to be that contracts (in the form of runtime assertion checks) may have to supplement compiletime typechecking to make the overall problem of verifying program correctness tractable.
I've been thinking for a while that it would be nice if there were some way that types and assertions could be unified. Types constitute a form of contract that is verified at compiletime (and/or loadtime, in languages that do loadtime verification), while assertions are verified at runtime. Runtime assertion checking is easy enough, so the difficulty in bridging the two is coming up with a general way to specify how contracts can be checked at compiletime: this requires giving your compiler and/or loader enough ammunition to do an automated proof, which is extremely hard except for the simplest cases (something like Java's nominal type system, before generics, constitutes a pretty simple case).
Eiffel is the only language I've seen that makes a big deal of method pre- and postconditions in a way that is analogous to typechecking on methods: that is, when you override a method m with a method m′, m′'s postconditions must be more specific than m's (covariantly), but its preconditions must be less specific (contravariantly).
It might be cool if a language had a sort of Third Way with respect to types and assertions, where you could tell the compiler to check a contract at compiletime if the compiler can figure out how (and it doesn't take too long), or at runtime otherwise. Runtime checking is generally inferior to compiletime checking, but most of us would settle for it if the compiletime check would take forever.
Subscribe to:
Post Comments (Atom)
Some people have called this Third Way "Hybrid Type Cheking". See for instance the Sage programming language [1]. Tools like ESC/Java have aimed at similar goals, without necessarily calling the contracts "types".
ReplyDelete[1] http://sage.soe.ucsc.edu/
I skimmed the Sage paper a while ago, and it was in the back of my mind. I'm thinking of a couple of things that I don't recall seeing there:
ReplyDelete. A way for the programmer to insist for a particular check whether it must be done at compiletime (the compiler complains if it can't carry it out); or must be done at runtime; or should be done at compiletime only if the compiler can prove the required condition quickly enough (or at all).
. Maybe some way to provide proof strategies or hints for certain types of contracts, rather than relying on a single preinstalled theorem prover.
Hmm, looks as if my wish list is getting out of control...