[dboreham]

Confused why the article author believes this is a surprise. The foundations of mathematics and computer science are basically the same subject (imho) and dualities between representations in both fields have been known for decades.

[sabellito]

If something people dedicated multiple years of their lives studying and proving seems trivial to you, you're either a genius or you didn't understand the problem.

[amoss]

There is a world of difference between the obvious and the trivial. The post you are replying to only implied it was obvious, the retort is unnecessary.

[kadoban]

It's not a surprise that math and CS are related. It's a surprise that this particular subject in math and CS are so intimately related.

[psychoslave]

Why? Both are basically about how to handle information with a priori indefinitely many cases, types, instances, species

[zmgsabst]

Is it?

The notion of algorithms and computer science were invented to discuss the behavior of infinite sequences: examining if there’s descriptions of real numbers. This was extended by connecting complicated infinite structures like the hyperreals with decisions theory problems.

That descriptions of other infinite sets also corresponds to some kind of algorithm seems like a natural progression.

That it happens to be network theory algorithms rather than (eg) decision theory algorithms is worth noting — but hardly surprising. Particularly because the sets examined arose from graph problems, ie, a network.

[Jweb_Guru]

I've done a bunch of theoretical PL work and I find this to be a very surprising result... historically the assumption has been that you need deeply "non-computational" classical axioms to work with the sorts of infinites described in the article. There was no fundamental reason that you could give a nice computational description of measure theory just because certain kinds of much better-behaved infinities map naturally to programs. In fact IIRC measure theory was one of the go to examples for a while of something that really needed classical set theory (specifically, the axiom of choice) and couldn't be handled nicely otherwise.

[zmgsabst]

Much of your comment seems to be about your culture — eg, assuming things about axioms and weighting different heuristics. That we prioritize different heuristics and assumptions explains why I don’t find it surprising, but you do.

From my vantage, there’s two strains that make such discoveries unsurprising:

- Curry-Howard generally seems to map “nice” to “nice”, at least in the cases I’ve dealt with;

- modern mathematics is all about finding such congruences between domains (eg, category theory) and we seem to find ways to embed theories all over; to the point where my personal hunch is that we’re vastly underestimating the “elephant problem”, in which having started exploring the elephant in different places, we struggle to see we’re exploring the same object.

Neither of those is a technical argument, but I hope it helps understand why I’d be coming to the question from a different perspective and hence different level of surprise.

[Jweb_Guru]

The reason people had these assumptions is because people have been trying (unsuccessfully) to find a constructive interpretation of this stuff for a very long time. Even very fundamental results in measure theory like the Heine-Borel theorem typically require some extension to traditional constructive axioms. Like I absolutely get where you are coming from, but there are a large number of "nice" classical results that definitely do not have constructive counterparts. It's cool that descriptive set theory is not one of them but it's not obvious by any stretch of the imagination, and the pattern you're using to say that it's probably true ("Curry Howard maps nice to nice") is not great process IMO since it would fail in a lot of other cases.

[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.

[zmgsabst]

Curry-Howard literally says that a proof your object has a property is equivalent to an algorithm which constructs a corresponding type.

I’m not “sprinkling magic powder”, but using the very core of the correspondence:

A proof that your network has some property is an algorithm to construct an instance of appropriate type from your network.

In this case, we’re using algorithms originally designed for protocols in CS to construct a witness of a property about a graph coloring. In the article, it details exactly his realization this was true — during a lecture, seeing the types of things constructed by these algorithms corresponding to the types of objects he works with.

[ben7799]

Reactions to your statement seem to hinge on whether or not the person replying has a CS degree from a math focused program!

It makes perfect sense to me.

[dandanua]

True. After Turing and Co, mathematical logic became almost like applied theoretical computer science.