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.
Saturday, September 17, 2011
Always in Beta
My quest to understand What Programming Languages Are Made Of has led to me start reading the Beta Programming Language book. I've only gotten as far as Chapter 3 so far, but I've already seen enough quirks in the language to have repaid the time.
If I see the implications properly, it looks as if Beta unifies method calls and object construction. That is, the language has no functions or methods per se; rather, all code lives in what would Java or Scala would consider constructors or instance initialization. Instance variables play the role of local variables.
It's easy to observe that stack frames are like objects, in that both are usually laid out as structs accompanied (in languages with managed memory) by a pointer to some sort of descriptor. But it's a bold leap to say that stack frames are objects.
I haven't read far enough to be sure that my understanding is correct. It would also be interesting to see whether Beta has any notion of alternate constructors—which, when viewing Beta objects as functions, would have an effect something like default function arguments.
Is the Beta approach part of the answer to the puzzle of What Are Constructors Made Of? I haven't figured that out yet.
I've seen Beta mentioned a few times, but never heard of anyone using for it anything. I wonder whether it failed to gain traction because people always assumed it was still in beta.
If I see the implications properly, it looks as if Beta unifies method calls and object construction. That is, the language has no functions or methods per se; rather, all code lives in what would Java or Scala would consider constructors or instance initialization. Instance variables play the role of local variables.
It's easy to observe that stack frames are like objects, in that both are usually laid out as structs accompanied (in languages with managed memory) by a pointer to some sort of descriptor. But it's a bold leap to say that stack frames are objects.
I haven't read far enough to be sure that my understanding is correct. It would also be interesting to see whether Beta has any notion of alternate constructors—which, when viewing Beta objects as functions, would have an effect something like default function arguments.
Is the Beta approach part of the answer to the puzzle of What Are Constructors Made Of? I haven't figured that out yet.
I've seen Beta mentioned a few times, but never heard of anyone using for it anything. I wonder whether it failed to gain traction because people always assumed it was still in beta.
Subscribe to:
Posts (Atom)