Comment by Jweb_Guru
3 days ago
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.
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.
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.