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. •Introducing a propositional logic with non-harmonious rules and the ⊙ (read “sup”) connective.•The proof language of this logic forms core of a quantum programming language.•Non-harmonious rules of ⊙ model quantum properties of measurement: info-erasure, non-reversibility, non-determinism.