Intro

Soundproof transforms formalized mathematical proofs (or propositions) into music, with the aim of producing a piece based on Girard's Paradox. The audio synthesis is built with FunDSP. The mathematical proofs are constructed in a custom Rust implementation of LambdaPi (originally in Haskell); Ilya Klyuchnikov's version was a particular model. Artistic influences include Iannis Xenakis, Catherine Hennix, Henry Flynt, Drexciya, Perturbator, Sun Ra, Karlheinz Stockhausen, and Odz Manouk.

It has two modes: single-term (--mode=term) and step-based (--mode=step). The single-term mode presents the tree structure across time, while the step-based mode presents the reduction behavior.

Output

The canonical output for the single-term mode is available for free download on Bandcamp. A screen recording of the live version is on Youtube.

The step-based mode does not yet have a canonical output.

A demo of this project, and a live performance of its output, was presented at the FARM workshop at ICFP/SPLASH 2025. The paper can be found in the FARM proceedings here, and a recording of the talk is available on the ACM SIGPLAN YouTube channel here. Video of the FARM performance should be available eventually.

How It Works

The lambda calculus is a formal system for computability, built around the concept of functions. Adding type systems to lambda calculi allows them to represent logical connections by having propositions as types and proofs as elements of those types. For example, a function from type A to type B takes a proof of proposition A and produces a proof of proposition B, which corresponds to logical implication. Dependent types can represent essentially all mathematical propositions, and dependently-typed lambda calculi are used as the basis for many theorem provers, including Coq/Rocq, Agda, and Lean.

This project's DTLC is based on LambdaPi, a very simple version of the DTLC whose first priority is ease of implementation. Notably, LambdaPi forgoes the universe hierarchy of usual dependent type theories for simplicity, so the type of Type is Type; this is essentially similar to the naive set theory idea of the "set of all sets", and leads to Girard's Paradox. LambdaPi was chosen partly for its simplicity but also because this paradox is the primary term I'm focusing on representing musically at the moment. The choice of a paradox is in part due to Henry Flynt's idea of "concept art", which would incorporate mathematics but reject the idea of "discovering" truths in favor of constructing beautiful concepts. This uses the simplified version of the paradox due to Hurkens.

Proof terms and types are structured naturally as trees, so we give each sort of term/type a little fragment of melody. Then, for a particular term/type we wish to translate, we give it a duration. We play the melody for the root of the tree over the whole duration, and then along with the root's melody we split up that duration and give it to the subtrees to play their translations in sequential order (potentially increased in pitch, etc. for distinction). The canonical output follows the call tree of the typechecker, which includes all the structure of a term's abstract syntax tree but additionally includes type structure for variables, which is important for lambdas.

Various desirable features of LambdaPi (equality types, etc.) have been left out for now, as they're not necessary for the paradox or for the musical side of the problem. They may be added eventually.

Additional Features

The single-term live performance mode is available on the bevy branch, and NOT on this one. It takes text input and parses it into terms which are then translated and displayed as moving trees along with the tags of the currently-playing subterms. Its display font is a modified version of JetBrains Mono which displays backslash as lambda.

The step-based live performance mode can take a path to a config file with a list of command-line options. By default, these will be stepped through sequentially; with the --midi option, they are mapped to MIDI notes and can be activated by a MIDI controller.

Notes

• Soundproof should always be compiled with --release, as the synth portions using FunDSP depend highly on optimizations that are not enabled in debug mode. It will not run in any reasonable time otherwise.

• The single-term live performance mode is unavailable on this branch due to dependency issues; switch to branch bevy to use it.

• The audio selectors names-short, names-long, and mixed pull from audio files in the files folder, which have not been included in Git for multiple reasons. The selectors' source in select.rs contains the relevant file names if you want to put in local replacements.

Usage

Usage: soundproof [OPTIONS]

Options:
  -m, --mode <MODE>              Whether to run the single-term or step-based translation [default: term] [possible values: single, steps]
  -l, --live                     Whether to render to file or run it live.
  -v, --value <VALUE>            Predefined terms of the dependently typed lambda calculus [default: sigma] [possible values: star, sets-of, u, tau, sigma, omega, lem0, lem2, lem3, girard]
  -r, --reduce                   When set, normalize the term as far as possible before being presented
  -t, --time <TIME>              In seconds. If unset, scales with size of tree. In step mode, determines time of one frame
  -d, --division <DIVISION>      Determines how time is broken down between sequential segments [default: weight] [possible values: even, weight, size]
  -c, --content <CONTENT>        Determines which audio selector to use, determining melodies, rhythm, timbre, and so on [default: full-stratified] [possible values: full-stratified, async-stratified, a, b, c, d, e, f, pure-sine, names-short, names-long, strat-instr, effects, mixed, loop, rhythmized, sine-rhythm, bare, tone-make]
  -s, --structure <STRUCTURE>    How to assign sound-tree structure to a term [default: type] [possible values: term, type, test]
      --freq-min <FREQ_MIN>      Low end of frequency range in step mode. Does nothing unless mode=steps [default: 60]
      --freq-max <FREQ_MAX>      High end of frequency range in step mode. Does nothing unless mode=steps [default: 2500]
  -S, --step-count <STEP_COUNT>  Maximum number of steps before quitting in step mode. Does nothing unless mode=steps
  -f, --filters <FILTERS>        Additional filters added after audio generation [default: clip-lowpass] [possible values: clip-lowpass, quiet, none]
      --step-file <STEP_FILE>    A file from which to load multiple configurations for stepping
      --midi                     Whether to take MIDI input for steps. Only works live
  -o, --output <OUTPUT>          Name of the output file [default: output.wav]
  -h, --help                     Print help (see more with '--help')
  -V, --version                  Print version