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 reduction behavior (--mode=reduce). The single-term mode presents the tree structure of proof terms across time, while the reduction mode presents terms as synth tones and their computational behavior as time. In the case of the paradox, this behavior is more "progression" than "reduction", as it grows larger eternally instead of reducing to a normal form.

Each mode has a live performance variant. These variants also generate visuals and provide opportunities for performers to intervene in the process.

Results

The canonical pieces for the single-term and progression modes are available for free on Bandcamp.

This project has been presented and performed at the ACM SIGPLAN FARM Workshop twice. The single-term version was at FARM 2025 at ICFP/SPLASH (paper, talk recording), while the reduction-based version was at FARM 2026 at ICFP (paper, talk recording).

I performed the single-term version at FARM 2025 (there is also a screen-only recording of this mode). I performed the progression-based version at FARM 2026. The recording will 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. They are either in a "normal" form, or they can take a step of "reduction" to move towards a normal form. However, the paradoxical term has no normal form. When "reduced", it grows in an endless cycle.

In the single-term mode, 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.

In the reduction mode, a single term is a synth tone/texture. Each sort of term/type has a waveform, and we translate the tree by dividing up pitch among the subtrees in the same way we divide duration above. The reduction of the term is then the evolution of these tones over time. Step duration can scale with the size of the change between one and the next, or can be fixed. The call-by and ann-step options control choices in the evaluation order.

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 due to version issues. 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. It also takes commands which set a four-note melody for a node type, e.g. set(Lambda=ADFA). Its display font is a modified version of JetBrains Mono which displays backslash as lambda.

The reduction/progression live mode can take a path to a config file with a list of command-line options. By default, these will be stepped through sequentially, generating sound and a visual representation of each term (highlighting the term's next step). For a performance, use the --midi option along with the --live option. In this mode, configurations are mapped to MIDI notes and can be activated by a MIDI controller. The mapping currently supports notes 48-73.

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. 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 reduction/progression translation [default: reduce] [possible values: single, reduce, reduce-variants]
  -l, --live
          Whether to render to file or run it live. Single-term live runs are currently unavailable on this branch
  -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 reduction 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]
  -f, --filters <FILTERS>
          Additional filters added after audio generation [default: clip-lowpass] [possible values: clip-lowpass, quiet, none]
  -o, --output <OUTPUT>
          Name of the output file [default: output]
  -L, --freq-low <FREQ_LOW>
          Low end of frequency range in reduction mode [default: 60]
  -H, --freq-high <FREQ_HIGH>
          High end of frequency range in reduction mode [default: 2500]
  -r, --reverse-freq
          Reverse frequency range in reduction mode
  -S, --step-count <STEP_COUNT>
          Maximum number of steps before quitting in reduction mode
      --reduction-config <REDUCTION_CONFIG>
          A file from which to load multiple configurations in reduction mode
  -D, --diff-time
          In reduction mode, whether to vary step time with the size of the change between steps. If `--midi` is enabled, turning this off means that steps will continue until the next MIDI note
      --call-by <CALL_BY>
          Evaluation order of function application in reduction mode [default: name] [possible values: name, value]
      --ann-eval <ANN_EVAL>
          Evaluation order of annotation dropping in reduction mode: whether the type and/or term should be evaluated before dropping the annotation if unnecessary [default: unprincipled] [possible values: neither, type, both, unprincipled]
      --midi
          Whether to take MIDI input for live reduction mode
  -h, --help
          Print help (see more with '--help')
  -V, --version
          Print version