Jason (jcreed) wrote,

Some pretty spectacular fireworks in class this morning; Karl covered a couple of interesting counterexamples that exercise dependent sum types and singleton types to show that certain approaches in IL design (pertinent to module systems) can't work. It has to do with the impossibility of solving something called the "Avoidance Problem". Karl said:

"Bob and I even had a system where we thought we had solved the Avoidance Problem, but it turned out not to work.
It was very sad.
I cried.
Well, I didn't really cry, but it was sad.
For a while I didn't work on the problem because of the trauma.
We gave up, because it [all but] seemed like God was conspiring against us.
The O'Caml approach is, 'well, who cares?'"

"What we'll come up with [in the rest of the course] is something less cool than O'Caml...
Unless what you mean by cool is 'something that works'."
Tags: classes

  • (no subject)

    I am blogging at some kind of pittsburgh blogging event blog blog blog. Goob is here, and Jen Landefeld. Not a bad deal so far.

  • (no subject)

    While searching for mathematical sheep jokes, I found this blog post by scott aaronson which contains a fable, which links to a counter-fable, which…

  • (no subject)

    Chris Onstad, genius creator of Achewood, is amusing today: Once in a great while I will allow myself to think that I have achieved something…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 1 comment