One is reminded of the difference between proof-relevant and classical mathematics. The letter of the law is a mere proposition, whereas the spirit of the law i

One is reminded of the difference between proof-relevant and classical mathematics. The letter of the law is a mere proposition, whereas the spirit of the law is a program of a certain type, whose “computational content” describes the actions one takes to produce the state of compliance.