Can real analysis be done point-free, for locales? That would be daunting to attempt in terms of frames and frame homomorphisms, but it has long been understood that an alternative is to use points and reason geometrically so that one is not just working with the global points (which may be insufficient).

My student Ming Ng developed real exponentiation and logarithms in this style. I have now arXived a paper (arXiv:2312.05228) that shows how to differentiate them. It relies on first proving the Fundamental Theorem of Calculus, after which the development is more or less conventional.

The style is quite natural, and reminiscent of Bishop’s constructive reasoning, though with a different mathematical trajectory. However, it is still an open question whether it is truly constructive in the sense of extracting algorithms from proofs. I have some notes on this, formatted as slides, at

  https://www.cs.bham.ac.uk/~sjv/GeologConsSlides.pdf

Steve Vickers.