Entirely joking about being offended, that work was a long time ago. I think it was an interesting exploration but we were not able to get compelling results, I think mostly because we did not at that time have affine types (move semantics). Thus if you put something into a container in one place and took it out in another, it would have to infer the region that spans both, which might as well be the whole program in most cases.
These days I program in Rust and find Rust's approach to explicit regions to be a workable compromise, though reference-heavy types can get pretty ugly and hard to work with (and I'm pretty sure that variance of lifetimes is confusing to everybody who isn't a PLT theorist and some who are).
The approach I personally find most interesting is the Lobster language. There (and I'm probably oversimplifying) the semantics are reference counting, but you so analysis to remove a huge fraction of RC operations. I believe the Perceus work is similar.
I'm happy to chat anytime. Recent work has been using somewhat exotic types provided by Rust (associated types, existentials, lots of inference through product types) to represent UI. So far I've basically been using what Rust gives me, but it's interesting to imagine what changes to the language/type system might buy you. For example, there are a few places in the code where there are downcasts, but I suspect that with a sufficiently strong type system you could prove those downcasts are infallible.
These days I program in Rust and find Rust's approach to explicit regions to be a workable compromise, though reference-heavy types can get pretty ugly and hard to work with (and I'm pretty sure that variance of lifetimes is confusing to everybody who isn't a PLT theorist and some who are).
The approach I personally find most interesting is the Lobster language. There (and I'm probably oversimplifying) the semantics are reference counting, but you so analysis to remove a huge fraction of RC operations. I believe the Perceus work is similar.
I'm happy to chat anytime. Recent work has been using somewhat exotic types provided by Rust (associated types, existentials, lots of inference through product types) to represent UI. So far I've basically been using what Rust gives me, but it's interesting to imagine what changes to the language/type system might buy you. For example, there are a few places in the code where there are downcasts, but I suspect that with a sufficiently strong type system you could prove those downcasts are infallible.