Demo: Rocq N’Roll

Rocq N’Roll is a software instrument and tool with type proof -> music. It parses Rocq proof tactics into Musical Instrument Digital Interface (MIDI) notes to generate musical sound based on a proof state. ’Playing’ or ’performing’ a proof with Rocq N’Roll means stepping through it interactively to generate pitches that correspond to the step in the proof, with more complex chords and melodies coming from proof steps with multiple suboperations (i.e. automated tactics). Rocq N’ Roll is primarily an artistic tool, but it may also have interesting use cases in helping Rocq users conceptualize proof deautomation. And (in our humble opinion) it sounds pretty sweet.