unison is currently the closest to showing how it is actually done

What makes you say that? As far as I’m aware, even the theoretical soundness of it isn’t a done deal (this is a harder nut to crack than e.g. rust’s borrow checker)

Overall, I think one of 2 things will happen:

In this niche, perhaps, I don’t believe any of those will gain mainstream adoption (though I hope I’m wrong)