  We investigate an unsuspected connection between logical connectives with
non-harmonious deduction rules, such as Prior's tonk, and quantum computing. We
argue that these connectives model the information-erasure, the
non-reversibility, and the non-determinism that occur, among other places, in
quantum measurement. We introduce an intuitionistic propositional logic with a
non-harmonious logical connective sup and two interstitial rules, and show that
the proof language of this logic forms the core of a quantum programming
language.
