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)

    Logic programming lately is a tiny bit unexciting because we are going over linear logic in detail. Surely we will be getting back to more strictly…

  • (no subject)

    Definitely had a more decent day today. Class was kind of interesting, and I got the homework for it done in the afternoon. Thanks to…

  • (no subject)

    Whoops, still not quite done with HOT. Two bugs left... --- I have found and fixed two bugs. Any of you familiar with the arithmetic of bugs knows…

  • 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