I work on developing better tools for solving computational geometry problems robustly and efficiently, so I got quite excited when this paper first appeared.
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...
