I'd be glad to discuss this over email if you like; the upshot is that I don't think there's anything formally proven anywhere along the way, but it might be in

I'd be glad to discuss this over email if you like; the upshot is that I don't think there's anything formally proven anywhere along the way, but it might be interesting to discuss if it theoretically could be (that is, given a hypothetical imperative language, is fork/join code possible to fully verify as I believe or not.)