This is a fantastic talk. I've watched a couple of different versions of this.

Towards the end he spoke about something in passing that's stayed with me.

Through out early/mid 20th century different mathematicians created their own theories of mechanised computation. Turing machine, Lambda calculus, SK combinators etc., However over they all turned out to be equivalent; for example Church-Turing thesis. So this leads one to believe strongly that mechanised computation is "discovered" rather than invented. Also it is a good indication that the computing theory is on a solid foundation.

However, when it comes to distributed and parallel computing theories have been proposed but no equivalence has been found (or at least proved). It's an active field which he hopes will result in a similarly solid foundation for the distributed computing. At the moment it seems to be on a shaky ground.

This three-part series of (long) posts is a very thorough and fascinating counterpoint to the idea that computation was discovered and that there is anything surprising about the confluence of lambda calculus, Turing machines etc, mostly using primary sources from Leibniz onwards:

"Finite of Sense and Infinite of Thought: A History of Computation, Logic and Algebra"

https://pron.github.io/posts/computation-logic-algebra-pt1

What is a distributed or parallel computing theory in this context? They can’t compute anything above and beyond sequential computers.

> However, when it comes to distributed and parallel computing theories have been proposed but no equivalence has been found

Is this really the case? It seems that game semantics ought to be able to model these concerns. The logical side of it would then be some sort of multi-modal logic.