In this informal talk I will tell the story of how we are extending
our methods for solving distributed computing problems in a Logic of
Events. Our goal is to solve problems in such a way that constructive
proofs of theorems contain distributed realizers from which the Nuprl
theorem prover can extract running code that solves the distributed
computing problem. The proof also gives an explanation of why the
algorithm is correct.