I haven't actually shared this blog with anyone, so this is the perfect place to write stream-of-consciousness about my latest semi-formed ideas. I'm trying to combine linear logic and pi calculus. I'm writing a whole database full of proofs in this system, although at the time of writing it is quite incomplete. This idea started out when I was searching for a way to model pi calculus. After realizing that classical logic is ill-equipped to reason about stateful procedures, I eventually discovered linear logic. The terms of linear logic can be interpreted as games against an adversary, with linear implication denoting the adversary's choice of moves. They can also be interpreted as resources traded between various sources and sinks, even alongside the game-semantic interpretation. So, I thought to myself, what if the games are between a programmer and a computer? (Some background on the two systems: Pi calculus can be thought of as a minimalistic, yet Turing-complete, ...