# I keep jumping around from past to present. I must be narrowing something down but I’m not sure what yet. “O’Hearn and Brookes are co-recipients of the 2016 Gödel Prize for their invention of Concurrent Separation Logic.” Just read: “Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity”, which uses the simple but fantastic notion of logical verification with TIMESTAMPS – AND using TWO histories simultaneously: SUBJECTIVE and Objective, allowing for things like dealing with programs that operate across networks, running concurrently, functions shared by the state space – even situations where it can decide not to do something if it was done by another program or by the state space itself. It’s part of https://en.wikipedia.org/wiki/Separation_logic – in this case, Concurrent Separation Logic. Why do I like this? If you abstract it’s function (take it out of the context of computer science), it’s logical reasoning that has PLACE and TIME and SUBJECTIVITY and multiple HISTORIES, features missing from many logics. Doing this gives the power to consider reasoning from TWO perspectives simultaneously: COARSE (objective, collective, hindsight) and FINE-GRAINED (subjective, individual, interactive, broken up).

I keep jumping around from past to present. I must be narrowing something down but I’m not sure what yet.

“O’Hearn and Brookes are co-recipients of the 2016 Gödel Prize for their invention of Concurrent Separation Logic.”

“Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity”, which uses the simple but fantastic notion of logical verification with TIMESTAMPS – AND using TWO histories simultaneously: SUBJECTIVE and Objective, allowing for things like dealing with programs that operate across networks, running concurrently, functions shared by the state space – even situations where it can decide not to do something if it was done by another program or by the state space itself.

It’s part of https://en.wikipedia.org/wiki/Separation_logic – in this case, Concurrent Separation Logic.

Why do I like this? If you abstract it’s function (take it out of the context of computer science), it’s logical reasoning that has PLACE and TIME and SUBJECTIVITY and multiple HISTORIES, features missing from many logics.

Doing this gives the power to consider reasoning from TWO perspectives simultaneously: COARSE (objective, collective, hindsight) and FINE-GRAINED (subjective, individual, interactive, broken up).
——–
Now looking at:
https://software.imdea.org/~aleks/ecoop17/ecoop17.pdf

Love this bit:

“A particularly troublesome case is when run-time information influences the logical order of a
procedure that has already terminated. “

======