Programming with spaces

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

Overview: 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 in a sound, semantically faithful manner. Committing to programming soundly with spaces ensures that all programs are continuous, which offers computational benefits in addition to ensuring robustness. But doing so also introduces its own challenges, and the principles of programming in this way have yet to be explored.

We are building a programming language for sound and robust computation on spaces in order to explore these principles, and exploring applications to areas including solid modeling and probabilistic programming.

People

Current:

• Ben Sherman
• Jesse Michel
• Michael Carbin

Past:

• Adam Chlipala
• Luke Sciarappa
• Jared Tramontano