Some pretty spectacular fireworks in class this morning; Karl covered…: jcreed

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'."

(no subject)

(no subject)

(no subject)

Error