Semantics-Driven Development (SDD)

A brief introduction

Maxine Levesque (@maxine.science) · Style note

What is SDD?

SDD is a method for the development of software systems. In SDD, you agree on the meaning of the system before you write the code. You write the meaning as mathematics. You then prove that the code obeys the meaning.

We use three words with special meanings:

• A denotation says what an object is. It is mathematics. It does not change when the code changes.
• A presentation is the finite data that identifies a denotation. A computer can store a presentation.
• A procedure is what the code computes. A correct procedure agrees with the denotation through the presentation.

Every claim of correctness in SDD has this form: the procedure decides, or approximates, the denotation through the presentation.

Why SDD helps

Confusion is the most costly part of design. SDD moves each type of confusion to the step where it costs the least.

• Confusion about the product is cheap in step 1.
• Confusion about the meaning is cheap in step 2.
• Confusion about the code is found by the proofs in steps 6 to 9.

A language model can now do step 2 with you at low cost. This changes the economics of formal methods. Before, you had to formalize while you were confused. Now you can remove the confusion first, in conversation, and formalize after.

The SDD loop

1. Do a design pass on intuition

Explore the product until you feel able to decide concrete details. Do not write formal text in this step. The output is shared intuition.

2. Write the denotational semantics

Do this in conversation, in natural language plus mathematics. Give each object its denotation, its presentation, and its procedure. Record each decision.

3. Formalize the semantics in Lean

Write the objects as types. Write the important claims as theorems. Prove the claims that protect the system (see What should I prove?). Mark the other claims as obligations.

4. Choose an implementation design

Decide how the system will realize the denotation in operation.

5. Write the operational semantics in Lean

Give enough detail to state the claims about operational behavior.

6. Prove the refinement

Show in Lean that the operational semantics is an instance of the denotation. Make this choice of relation in step 3, because it controls how you must write step 5.

There are three types of proof. Choose one type for each law.

• Equation. Two procedures give equal results. Example: mask then truncate equals truncate then mask.
• Simulation. Each concrete step matches an abstract step through an abstraction map. Example: an incremental index simulates the derived structure.
• Bisimulation. Two objects cannot be told apart by any observation. Example: two records that unfold to the same tree at every depth.

Bisimulation needs coinductive proof machinery. Plan for this in step 3.

7. Build the software

Do this in parallel with step 5.

8. Connect the software to Lean

Generate a type that specifies the software. Use the adoption ladder below.

The ladder has three rungs. Start at the bottom rung. Climb only where proofs pay.

• Rung C — specification tests. Generate property-based tests from the interface laws. Run the tests in CI. This gives the main benefit in the first week. There is no proof of the code.
• Rung B — embedding. Translate the core of the code into Lean. Prove against the translation. The remaining gap is the fidelity of the translation. You can test that gap.
• Rung A — extraction. Write the component in Lean. Extract the code from Lean. This gives the strongest guarantee. It also removes your usual language and libraries. Use it only for small, critical components.

9. Assemble the full proof

Show that the software is an instance of the denotation. Run this check in CI.

Iterate

Design changes will reopen step 2. This is normal. The method stays useful because of the ledger.

The ledger is a list with two parts:

• Settled items. Decisions that are made, with their reasons.
• Open items. Questions that are not decided, each with a home: the layer where the decision belongs.

A change request must name the ledger items it touches. The CI gap report speaks about ledger items, not about files. The ledger is a required output of step 2.

What should I prove?

Do not prove everything. Prove the claims that protect something important. We call these the critical theorems. Examples from our project:

• Growth soundness: old data stays valid when the schema grows.
• The incidence fence: free structure cannot create paid structure. This is a security property.
• Fence persistence: a coarser view cannot create new connections.

Keep cryptographic assumptions as named axioms. Put them at one boundary in one file. A proof with hidden assumptions is not much better than no proof.

How to start

1. Hold the design conversations. Stop when details feel decidable.
2. Write the denotational semantics document and set up the iteration ledger.
3. Transcribe the denotation as mechanized Lean. State all the laws. Prove the critical ones.
4. Build the implementation and its operational semantics. Prove that the implementation is an instance of the denotation.
5. Automate generating implementation tests from the critical laws’ refinements. Add these, the abstract law proofs, and the operational refinement proofs to CI.
6. Iterate. When a gap appears, the ledger tells you which decision it touches.

The Lean implementation

The type layer for SDD is sdd-lean. It gives the objects in this primer as Lean types. It provides the triple, the three refinement relations, the ledger, and the reusable CI checks. A repository imports it and proves its module boundaries against it.

Style note. This primer uses the rules of Simplified Technical English (ASD-STE100) where possible. Sentences are short. Each sentence gives one idea. The voice is active. Special terms are defined before use.