Patch
A change-oriented programming language and browser IDE. Patch represents semantic state changes explicitly, infers contracts, records provenance, and connects selected evidence to Lean 4 checks.
Programs described through state changes
Patch makes changes to semantic state the central programming construct. The browser IDE exposes the language, inferred contracts, provenance, and evidence without requiring a local toolchain for the first evaluation.
The project studies whether change-oriented representation can make effects, assumptions, and verification obligations easier to inspect than conventional source alone.
- 01Explicit semantic state changes
- 02Inferred contracts and visible obligations
- 03Provenance attached to program changes
- 04Lean 4 checks for selected formal evidence
Making change and evidence inspectable
The research direction combines programming-language design, provenance, contract inference, and formal verification. The web environment supports small, reproducible examples that can be inspected without installing the compiler stack.
Patch also separates executable behaviour from evidence about that behaviour, so an interface can show which properties are inferred, asserted, or formally checked.
Evidence boundary
Patch is a beta language and IDE. Lean-checked evidence applies only to the properties and generated obligations actually represented in the verification path; it is not a blanket proof of arbitrary programs.