Cyclone and Curry-Howard
However what I did glean from the discussion was that Cyclone’s straightforward memory leak detection algorithm doesn’t lead to a small, well-defined interface. Case in point: in order to implement a garbage collector they had to extend the runtime. It was a small function (only 5 lines of code) but nevertheless it was not possible at the user level. In effect, they had to introduce a new proof rule into the type system. That’s disturbing to me—it means the type system is incomplete. And these are smart people, so if it wasn’t complete to start with, that probably means it’ll never be complete.
Cocoa programmers might find that Cyclone’s regions look a little familiar.
