Formal model for defender method resolution

Brian Goetz brian.goetz at
Thu Jan 20 07:17:11 PST 2011

Quite so.  The whole point of a formal model is precision.  There 
already is an English description (the document that was posted months 
ago), but English has the problem that things can rarely be made as 
precise as you'd like.  So the English document is good for capturing 
the basic idea.  Eventually, we will produce a specification in English 
as well, but most people don't find that all that readable either (and 
it is also easy to commit precision errors when writing language 
specifications, as the number of spec bugs over the years will attest.)

This document is an intermediate product so that we can ensure that 
we're discussing the same thing, and is intended to be useful in 
refining the design, developing the implementation, and writing the 
spec.  At which point it will be in code and English.

If you'd like to learn more about the approach used in this document, I 
highly recommend Pierce's "Types and Programming Languages" 
  It requires very little background in math or theoretical computer 

PS.  If you think this one is dense, you should have seen the previous 
draft.  This is the simplified version!

On 1/20/2011 9:31 AM, Mark Thornton wrote:
> On 20/01/2011 14:01, Collin Fagan wrote:
>> Okay, I'm officially out of my depth. This looks like math and I was never
>> good at math. Is the English/java for this really so verbose as to require
>> this massively abbreviated syntax? It's a six page document, if the syntax
>> is ten time more expressive/terse then I can see not wanted to write 60
>> pages. But if it's only twice as abbreviated the would not a 12 page
>> document reach more people?
>> Collin
>> On Wed, Jan 19, 2011 at 11:48 AM, Brian Goetz<brian.goetz at>wrote:
> It is a formal model. While it might be possible to write entirely in
> English it probably wouldn't be English as you know it:
> "Mathematicians are like Frenchmen: whatever you say to them they
> translate into their own language and forthwith it is something entirely
> different." -- Johann Wolfgang von Goethe
> The abbreviation is for formality and accuracy and not merely for
> compactness.
> Mark Thornton
> PhD, Mathematics

More information about the lambda-dev mailing list