Matthew Mandel

We were recently looking at a new crypto protocol at USV. As we were discussing it as a team, we realized we didn’t totally understand how the protocol worked. Even worse, we found it hard to precisely articulate our questions about the protocol to each other.

After some discussion in natural language, our partner Albert suggested we write up an interpretation of the protocol in pseudocode and have the founder review it. By writing an interpretation in pseudocode, we were able to unambiguously specify a protocol, and with the founder’s feedback, we revised it to be the right one. We realized that by using a formal language like (pseudo)code, we could communicate more carefully and clearly.

Philosophers have long struggled with the challenges posed by the ambiguity of language when trying to reason about a priori truths. Aristotle made some early progress with his syllogistic logic, establishing a foundation for formal reasoning. In the 19th century, figures like George Boole and Gottlob Frege expanded this foundation. They developed a system of symbols and rules for the expression of complex propositions, the definition of relationships between them, and the derivation of valid conclusions. These advances in logic paved the way for the birth of Computer Science, which gave us the ability to rigorously talk about algorithms. Software developers use this technology everyday to tell computers what they should do. And I think the rest of us could probably benefit from communicating more formally as well.

One recent example where formal expression should’ve been used is the Supreme Court case Pulsifer vs United States. The decision revolves around how to interpret a law that says courts must use federal sentencing guidelines (instead of statutory minimums) if:

“(1) the defendant does not have—

(A) more than 4 criminal history points, excluding any criminal history points resulting from a 1–point offense, as determined under the sentencing guidelines;

(B) a prior 3–point offense, as determined under the sentencing guidelines; and [emphasis added]

(C) a prior 2–point violent offense, as determined under the sentencing guidelines;”

The big question the Supreme Court debated was whether the enumerated conditions were meant to be disjunctive (any of them are sufficient to trigger the use of federal guidelines) or conjunctive (all jointly necessary to trigger the use of federal guidelines). Those are two radically different interpretations of a law that presumably had a single intent behind whether it wanted to make it easier or harder to avoid minimum sentences. And worse, the Court was split on the question of how to interpret it. This question – and any others like it – would be entirely avoided if Congress dealt with logical propositions more formally when writing conditions like these into bills. I’m not sure how much that would move the needle in improving Congress, but it seems like low-hanging fruit worth picking.

One more domain in which formal expression may become increasingly important is communicating with AIs. Part of the magic of LLMs is that they allow us to interface with computer systems in natural language; eg natural language interfaces to coding AIs allow anyone to become a programmer by just describing what functionality they want implemented. However, if Congress struggles to unambiguously specify its intention in natural language, we should expect human prompters to hit a similar roadblock. Learning to express ourselves formally (whether that’s just incorporating Boolean operators as savvy Google searchers might or writing full algorithms in pseudocode) might become an important way to ensure our intentions are correctly executed by AIs– just as Congress can better ensure its intentions are correctly carried out by the courts.

Writing clearly in natural language is hard! Using some of the tools of formal expression can make it a bit easier.

Thanks to Abigail Simon for helpful discussion and reading drafts of this post.