[a_tartaruga]

> He wanted to show that every efficient local algorithm can be turned into a Lebesgue-measurable way of coloring an infinite graph

To me this is quite surprising. Distributed systems were not designed to solve measure theory problems.

[jsrozner]

Perhaps it’s that a global solution in the language of set theory was hard to find, but distributed systems — which need to provide guarantees only from local node behavior, without access to global — offered an alternate perspective. They weren’t designed to do so but they ended up being useful.

[Ar-Curunir]

> They weren’t designed to do so but they ended up being useful.

an object doing something that it wasn’t designed for seems to me to be the definition of “surprising”

[zmgsabst]

They’re literally exploring the same object: properties of networks.

That you can express the constraints of network colorings (ie, the measure theory problem) as network algorithms strikes me as a “well duh” claim — at least if you take that Curry-Howard stuff seriously.

[Ar-Curunir]

Curry-Howard is not some magic powder you can just sprinkle around to justify claims. The isomorphism provides a specific lens to move between mathematics and computation. It says roughly that types and logical propositions can be seen equivalently.

Nothing in the result in the article talks about types, and even if it could be, it’s not clear that the CH isomorphism would be a good lens to do so.