Design by Contract and effects are essential for LLM-generated code

AuthorsNameGavin RayTwitter@GavinRayDev<br>In this post, I want to discuss two language features that I think have become substantially more important as software development shifts from human-authored to LLM-authored code.<br>Like many others, the majority of the code I have "written" (prompted) and shipped in the last year was not authored by me. You feed specifications to an LLM, it spits out an implementation, and you ask it to write tests to verify the behavior. You run the tests, manually poke the app to see if it behaves how you expect, and if you have the time you review the code.<br>This sort of development loop gives immense value to "code that verifiably does what it says on the tin."<br>There are two programming language features that facilitate this, and I'm convinced that their value is tenfold in this new era of machine-generated code:<br>Design-by-Contract<br>Effects<br>The net result of these is the possibility to have compiler-generated reports of semantic changes in a PR, like:<br>Effects added: PaymentProcessor.process<br>+ net.connect<br>+ retry.nondeterministic

Postcondition weakened: Ledger.append<br>- ensures ledger.length == old(ledger.length) + 1

AI (Dis)use Disclaimer: No part of the prose was machine-generated. You will not find machine-written prose on this blog. I consider it deeply disrespectful.

Design-by-Contract<br>Design-by-Contract (DbC) is language/syntax feature that allows writing preconditions, postconditions, and invariants (always-true) as part of the signature of methods and structs/classes.<br>It's somewhere between a mix of ad-hoc testing and formal specification. In many languages, contracts have build-time "level" switches which toggle the behavior and checks from compile-time to run-time, for performance reasons.<br>A picture is worth a thousand words, so rather than continue describing Contracts, let me give some (hopefully) self-explanatory examples.<br>Suppose we have a User type:<br>struct User {<br>email: String<br>email_verified: Bool

Nothing prevents this state:<br>User {<br>email: "",<br>email_verified: true

But with Design-by-Contract, we can encode a few simple invariants to rule it out:<br>struct User {<br>email: String<br>email_verified: Bool

invariant email.is_valid_email()<br>invariant email_verified implies !email.is_empty()

Changing the email can then specify what else must change:<br>fn change_email(user: &mut User, new_email: String)<br>requires new_email.is_valid_email()

ensures user.email == new_email<br>ensures user.email_verified == false

Without the postcondition ensures, a generated implementation might update the address while leaving email_verified set to true.<br>Data structures whose properties can be encoded as invariant conditions are particularly well suited to this sort of design:<br>struct MinHeapT: Ordered> {<br>items: ArrayT>

invariant forall i in 1..items.length:<br>items[parent(i)] items[i]

struct BTreeNodeK, V, const ORDER: usize> {<br>keys: ArrayK><br>values: ArrayV><br>children: ArrayNodeRef>

is_leaf: bool

invariant keys.length == values.length<br>invariant keys.length ORDER - 1

invariant strictly_increasing(keys)

invariant is_leaf<br>implies children.length == 0

invariant !is_leaf<br>implies children.length == keys.length + 1

Effects<br>Effects are a way to denote explicit capabilities in methods.<br>Typically these are behaviors such as "file/network IO, memory allocation, state changes", etc. By requiring that method effects be explicit, you can use a method's signature as a verified contract of its permitted behaviors.<br>As one example, suppose we have a method:<br>fn load_settings(path: Path) -> Settings

The return type says nothing about where the settings come from or what the operation may do.<br>An effect-aware signature does:<br>fn load_settings(path: Path) -> Settings<br>requires path.exists()<br>requires path.is_file()

ensures result.is_valid()

effects {<br>fs.read(path),<br>alloc

Now compare that with a function that merely parses settings already held in memory:<br>fn parse_settings(contents: String) -> Settings<br>requires !contents.is_empty()

ensures result.is_valid()

effects {<br>alloc

These functions may return the same TYPE, but they have meaningfully different OPERATIONAL behavior. That difference should be visible at the call site.<br>A few more examples:<br>Cache get that updates recency internal metadata<br>At first glance, you might think that the below method is read-only:<br>fn get(cache: &mut CacheK, V>, key: K) -> OptionV>

But many caches maintain usage statistics, and it may be the case that our get method is mutating. The below signature is explicit about behavior like this:<br>fn get(cache: &mut CacheK, V>, key: K) -> OptionV><br>ensures result.is_some() == old(cache.contains(key))<br>ensures cache.entries == old(cache.entries)

effects {<br>state.write(cache.recency)

The cache contents do not change, but its eviction metadata does.<br>A function that must not allocate<br>Suppose that we have a method which writes/encodes some value into a caller-supplied buffer:<br>fn...