Lambda the Ultimate

Games industry curmudgeon and interactive storytelling proponent Chris Crawford spoke at the Game Developers Exchange conference here in Atlanta yesterday. As a part of the talk he explained the "Nine Breakthroughs" that were important to his work on Storytron. I recorded them here...

Surprisingly, many of the ideas are about languages - either the programming languages used to program the games, or the language interfaces provided to users.

I'd think I want to allow a function with this type:

proc(class T cls) : T

And I want such functions to support type subclasses. For a simple instantiating example:

proc myfun(class Employee empcls) : Employee
return empcls.new()
...
Manager m = myfun(Manager);

Where

class Manager(Employee)
bonus : Dbl = 2.5 * salary; // :-)

Is this "principle of least surprise"? commonplace? or are there gotchas I'm not thinking about.

Thanks much.

Scott

I've read this site for some time, but now I have a question I believe the people at LtU could answer. The question is what are some of the current applications of formal semantics.

I've read or skimmed through some semantics textbooks, like Winskel's, and some less well-known, but a question they rarely answer in a satisfactory manner, at least to me, is why I should try to model the semantics of a language formally in the first place. Usually, the books say in the very beginning that semantics is useful for verification and program analysis, and then say no more about it. That's the reason I tried to get hold of a copy of Semantics with Applications as soon as I discovered it (an old edition is available online). The applications mentioned in the book are proving the correctness of an implementation, program analysis, and axiomatic program verification.

I've also seen recently the papers about expressing semantics in theorem provers, like here. It's cool that it is possible to extract an interpreter and a module for program analysis from the proofs about semantics. But we could just code the interpreter and program analysis; yes, I know, extracting them from a prover makes them more trustworthy. I refrain from saying that they are "correct" because it would depend on the correctness of the theorem prover, the compiler for the language, the extraction process, etc. Also, I don't know how this idea would fare in bigger, more realistic languages.

So, although I have seen already some applications of formal semantics, nothing of it quite managed to impress me much. What is it, then, that we gain by modeling the semantics of a language formally? What we can accomplish with a semantics that we couldn't without? What would be possible without a formal semantics, but difficult and/or clumsy? What examples do we have of sucessful and important applications of formal semantics to programming practice?

I think this is very much worth knowing, the questions are worth asking, and the books don't provide answers. So maybe LtU can :)