I can't comment on whether or not this will definitely be the future of programming, though I do think it's interesting. The more interesting thing to me is ju

I can't comment on whether or not this will definitely be the future of programming, though I do think it's interesting. The more interesting thing to me is just the idea of separation logic. The functional programming community has this idea that functional programming is the only sound programming model from a logical perspective, because it is very historically rooted in math and logic. Turing machines, by contrast, are much more 'made-up' constructions - they have weird, non-mathematical sounding components like heads and tapes, etc. But, for whatever reason, we can produce extremely fast and small processors that pretty closely resemble Turing machines, and C-style imperative, memory-based code flows naturally from that. And, with separation logic, it can also be firmly rooted in math and logic. That was always my feeling with the functional programming zealots, like they were just ignoring other possible universes. The lambda calculus is one formally sound model of computation, sure, but surely it's not the only one.