Verification and Transparency

Link post

Epistemic sta­tus: I’ve thought about this topic in gen­eral for a while, and re­cently spent half an hour think­ing about it in a some­what fo­cussed way.

Ver­ifi­ca­tion and trans­parency are two kinds of things you can do to or with a soft­ware sys­tem. Ver­ifi­ca­tion is where you use a pro­gram to prove whether or not a sys­tem of in­ter­est has a prop­erty of in­ter­est. Trans­parency is where you use tools to make it clear how the soft­ware sys­tem works. I claim that these are in­ti­mately re­lated.

Ex­am­ples of verification

Ex­am­ple of transparency

How ver­ifi­ca­tion and trans­parency are sort of the same

Apart from aes­thetic cases, the pur­pose of trans­parency is to make the sys­tem trans­par­ent to some au­di­ence, so that mem­bers of that au­di­ence can learn about the sys­tem, and have that knowl­edge be in­ti­mately and nec­es­sar­ily en­tan­gled with the ac­tual facts about the sys­tem. In other words, the pur­pose is to al­low the users to ver­ify cer­tain prop­er­ties of the sys­tem. As such, you might won­der why typ­i­cal trans­parency meth­ods look differ­ent than typ­i­cal ver­ifi­ca­tion meth­ods, which also have as a pur­pose al­low­ing users to ver­ify cer­tain prop­er­ties of a sys­tem.

How ver­ifi­ca­tion and trans­parency are different

Ver­ifi­ca­tion sys­tems typ­i­cally work by hav­ing a user spec­ify a propo­si­tion to be ver­ified, and then at­tempt­ing to prove or dis­prove it. Trans­parency sys­tems, on the other hand, provide an arte­fact that makes it eas­ier to prove or dis­prove many prop­er­ties of in­ter­est. It’s also the case that en­gage­ment with the ‘trans­parency arte­fact’ need not take the form of com­ing up with a propo­si­tion and then at­tempt­ing to prove or dis­prove it: one may well in­stead in­ter­leave prov­ing steps and speci­fi­ca­tion steps, by look­ing at the arte­fact, hav­ing in­ter­est­ing lem­mas come to mind, ver­ify­ing those, which then in­spire more lem­mas, and so on.

In­ter­me­di­ate things

Think­ing about this made me re­al­ise that many sorts of things both serve ver­ifi­ca­tion and trans­parency pur­poses. Ex­am­ples:

  • Type sig­na­tures in a strongly typed lan­guage can be seen as a method of en­sur­ing that the com­piler proves that cer­tain er­rors can­not oc­cur, while also giv­ing a hu­man read­ing the pro­gram a bet­ter sense of what var­i­ous func­tions do.

  • A math­e­mat­ics text­book con­tain­ing a large num­bers of the­o­rems, lem­mas, and proofs is made by prov­ing a large num­ber of propo­si­tions, and al­lows a reader to gain an un­der­stand­ing of the rele­vant math­e­mat­i­cal ob­jects by pe­rus­ing the the­o­rems and lem­mas, as well as by look­ing at the struc­ture of the proofs.