These are chat archives for jdubray/sam
That's pretty accurate! (I'm one of the authors.)
Our basic idea is that futures correspond very closely to the interpretation of the "eventually" operator in temporal logic. So if we could give a typed lambda calculus for temporal logic, then we could implement the eventually operator with futures. The benefit of doing this is that we could design languages which combine the easiness of reasoning featured by purely functional programming, while still offering good support for event-based programming (eg, for GUIs). In addition, if we are coming from a typed language that has enough invariants, we can also simplify the implementation of futures (since we know statically that certain problems like deadlock can't arise).
My personal goal is to figure out the fundamental primitives of interactive programming. Ultimately I'd like to be able to go from a framebuffer to a comfortable GUI toolkit in a few hundred lines of code, so that teaching the principles of how to implement these things can fit into a semester-long course. (Since there is a fairly small limit on how much code a student can reasonably write/comprehend in a term, the better we understand a problem the more we can teach.)