We are building a programming language for manipulating topological spaces (such as real numbers or probability distributions) in a sound manner, where all functions are continuous.

Software routinely manipulates continuous concepts, such as space, time, magnitude, and probability. However, such software usually does so with unsound approximations, such as using floating point rather than real numbers. These approximations can result in errors and also make it very difficult to reason about program behavior. Instead we propose to program with topological spaces themselves, in a semantically faithful manner. Committing to programming with spaces in this manner ensures that all total programs are continuous, which offers computational benefits in addition to facilitating reasoning. But doing so introduces its own challenges, and the principles of programming in this way have yet to be explored. We are building a programming language, based on constructive topology and embedded within Coq, in order to explore these principles.