Ack, my apologies, I didn't intend to be so inflammatory! If memory serves AFL was one of the first schemes (or perhaps the first?) to abandon the stack discipline to provide better inference in quite a few cases compared to TT. I remember the graphs in that paper giving me more hope for region inference to be a practical memory management scheme. Later, I believe the imperative regions paper improved on the AFL scheme a bit at least in their single 'life' example, but without more test cases or graphs it is more difficult in general to assess that paper or how common this case matters in practice.
I'm curious what you believe the future of research for region inference to be considering most of the papers written after TT's retrospective paper seem to have moved in the direction of explicit regions rather than inferred ones.
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.
I’m curious what the rationale is for not making regions explicit in the source code. It seems like a downside of region inference for a systems language is the unpredictability of the inferred regions.