Refine yourself a code
for great good!

Shaowei Lin [Atlas] [BAIF]

2025-05-30 Relatorium

Recreational Vibe Coding

Professional Vibe Coding

Vibe Coding in Cursor

For Great Good!


Challenge is to scale verified coding for

  • a human (with little formal training)

  • a human assisted by AI (and their hallucinations)

  • a human team assisted by AI (through building trust)

Today’s Take-homes

Refinement

  • Small incremental
    goal decompositions
  • Opposite of interactions
    between interfaces

Today’s Take-homes




Translation

  • Mapping between
    interfaces and interactions
  • Double categorical perspective

Compassionate Coding


Kindness via
Refinement

  • Not starting with all the
    requirements or answers
  • Allow for mistakes and
    learning from them
  • Construct by refining
    our specs and solution

Honor via
Translation

  • Language encodes our values
    and the way we think
  • Honoring the language of others
    and connecting them with ours
  • Collaborate by translating
    our specs and solutions

Refinements

Refinements

Insert Function - Signature

Insert Function - Refinement

Insert Function - Refinement

Insert Function - Finished

Interfaces and Interactions

Interactions (open systems; wiring diagrams) with their
external and internal interfaces. Composition occurs by nesting.

Interfaces and Interactions

Theorem Proving

  • Tactics refine goals into subgoals
  • Under the hood, a partial proof term eventually glues proofs of the subgoals into a proof of the original goal

Theorem Proving

Example. The induction tactic

theorem plusR_zero_left (k : Nat) : k = Nat.add 0 k := by
  induction k

generates the following two subgoals

⊢ 0 = Nat.add 0 0

n✝ : Nat
a✝ : n✝ = Nat.add 0 n✝
⊢ n✝ + 1 = Nat.add 0 (n✝ + 1)

and the partial proof term

fun k => Nat.recAux ( ) ( ) k

Translations

Maps between Interfaces

Language workbench demo (2009) from stealth startup Intentional Software

Changing representations in “projectional editing”

Maps between Interfaces

Maps between Interactions

Reflection between logical predicates and boolean functions.

Maps between Interactions

Complex maps between logical predicates and boolean functions can be composed from simpler maps.

Lemma idP : reflect b1 b1.
Lemma idPn : reflect (~~ b1) (~~ b1).
Lemma negP : reflect (~ b1) (~~ b1).
Lemma negPn : reflect b1 (~~ ~~ b1).
Lemma negPf : reflect (b1 = false) (~~ b1).
Lemma andP : reflect (b1 /\ b2) (b1 && b2).
Lemma orP : reflect (b1 \/ b2) (b1 || b2).
Lemma nandP : reflect (~~ b1 \/ ~~ b2) (~~ (b1 && b2)).
Lemma norP : reflect (~~ b1 /\ ~~ b2) (~~ (b1 || b2)).
Lemma implyP : reflect (b1 -> b2) (b1 ==> b2).

Managing Interfaces and Interactions

  • Representation \(\leftrightarrow\) Interface. Projection \(\leftrightarrow\) Translation. Generation \(\leftrightarrow\) Refinement
  • But do we really need a centralized abstract representation?


Traditional compilation

Language workbench

Double Categories

A (pseudo-)double category is a
category internal to \(\text{Cat}\), i.e.

  • category \(C_0\) of objects

  • category \(C_1\) of morphisms

  • source, target functors \(s, t: C_1 \rightarrow C_0\)

  • identity-assigning functor \(e: C_0 \rightarrow C_1\)

  • composition \(c: C_1 \times_{C_0} C_1 \rightarrow C_1\)

Double Categories

  • objects: objects of \(C_0\)

  • \(\downarrow\) tight morphisms: morphisms of \(C_0\)

  • ⇸ loose morphisms: objects of \(C_1\)
    (we only assume associativity holds
    up to coherent isomorphism)

  • \(\Downarrow\) cells: morphisms of \(C_1\)

Double Categorical Systems Theory

  • objects:
    interfaces

  • tight morphisms:
    interface maps

  • loose morphisms:
    interactions

  • cells:
    interaction maps

Poset of Refinements

  • Add checkpoints with git
  • Backtrack when implementation is stuck
  • Backtrack when specification is updated

Blueprint for Coordination

  • Blueprint (Patrick Massot) for coordinating collaborative theorem proving
  • Build a Blueprint for the double category of refinement and translations?

VeriLib

SpecIDE

Tool for spec translation (autoformalization), refinement and analysis

Aside: CatColab

https://catcolab.org/ for defining and computing with doctrines, theories,
models and instances within a double categorical framework.

Scaling Verified Coding


Humans (with little formal training)

  • Write verified code by choosing from a menu of refinement tactics

Humans assisted by AI (and their hallucinations)

  • Code synthesis via sampling tactics, not sampling tokens

Teams assisted by AI (through building trust)

  • Blueprint for the double category of refinements and translations

Thank you : )

https://shaoweilin.github.io/