I wonder if anyone has thoughts on the approach taken here ("Sound and robust solid modeling via exact real arithmetic and continuity"): https://icfp19.sigplan.org/details/icfp-2019-papers/15/Sound...
However, while the type theoretic developments based on Abstract Stone Duality is interesting, they mostly ignore the problem of efficiency by simply representing every real number as a Dedekind cut. Thus, it doesn't scale without significant advances in compiling real arithmetic. A problem I'm working on presently, but it might take a few years...