Let's not make a fuzz about it

Abstract

The work of Fuzz has pioneered the use of functional programming languages where types allow reasoning about the sensitivity of programs. Fuzz and subsequent work (e.g., DFuzz and Duet) use technical devices like linear types, modal types, and partial evaluation. These features usually require the design of a new programming language from scratch - a major task on its own! While these features are part of the classical toolbox of programming languages, they are often rather obscure for non-programming language experts. In this work-in-progress talk, we explore a different direction. We propose the design of a library capable of calculating the sensitivity of programs. The library is built on a novel use of polymorphism to represent (and prove) the sensitivity of functions together with the use of type constraints and type-level natural numbers. We show how our approach can be used to reason about the sensitivity of classical examples working over vectors, such as sum, map, and sort - we leave reasoning about more complex programs for future work. We will also present some future directions to explore together with some flaws that our approach that we need to overcome.

Date
Feb 19, 2021 1:15 PM
Event