Lean's unfair advantage
SF LEAN · ALOK SINGH · JULY 21, 2026
An ordinary programming languagewith a reason not to become Python
records · functions · errors · Clifford algebra · a typed InfoView boundary
0:00-0:20. Open with the title, not the Scarf conclusion.
Say: “This is a talk about Lean as a normal programming language. The spicy
version is that Lean may be better positioned than Haskell—not because it is a
better Haskell, but because it has a second job that is much harder to replace.”
A Haskell story, accurately
7 years Haskell in Scarf production
held up reliability, types, performance
new API work now goes into Python
the tax build time, ecosystem, agent feedback
Not a big-bang rewrite. Existing Haskell still runs while its footprint shrinks.
Avi Press, “After 7 years in production, Scarf has reluctantly moved away from Haskell,” July 10, 2026
0:20-1:05. Be exact. Avi Press says Haskell delivered reliable code, caught
real bugs, and performed well. Scarf started putting new API work in a Python
server; the existing Haskell server still runs and is being reduced gradually.
The stated costs were compilation time and ecosystem friction, amplified by
parallel agent workflows.
Do not say “Scarf deleted all its Haskell.” The accurate version makes the
argument stronger.
My inference, not Scarf's
A language is vulnerable when its distinctive value becomesorganizationally substitutable.
So what does Lean offer that “Python + more tests” does not?
A continuum from executable model to machine-checked specification and proof.
1:05-1:40. Mark the inference clearly as yours.
Say: “The interesting question is not whether Python is bad, or whether Haskell
is bad. It is what remains distinctive when code generation makes an
application cheap to port. My bet is that Lean has a stronger answer.”
One language, two jobs
JOB ONE
Build the program
strict functional code
arrays, loops, IO, errors
native compilation and Lake libraries
+
JOB TWO
State why it is right
dependent types
propositions and proofs in the language
a small kernel checks the result
Lean is officially described as both a programming language and proof assistant · lean-lang.org
1:40-2:10.
Say: “Python alone can replace an application. Replacing a Lean application
that also serves as its checked specification changes the product. But Lean
only earns that advantage if job one is real—if it can do boring programming.”
The boring part is the point
structure PlanarGrid where
xCount : Nat
yCount : Nat
def sampleCount ( grid : PlanarGrid ) : Except String Nat := do
if grid . xCount < 2 then
throw "xCount must be at least 2"
return grid . xCount * grid . yCount
#eval Except.ok 9 sampleCount { xCount := 3 , yCount := 3 }
Except.ok 9
#eval Except.error "xCount must be at least 2" sampleCount { xCount := 1 , yCount := 3 }
Except.error "xCount must be at least 2"
This slide is a Lean file. Verso type-checked the code while building the deck.
2:10-2:35. Click sampleCount if you want Verso's code info panel, but do not
linger. This slide is also the fallback if the editor is unavailable.
Say: “A record, a function, an explicit error, and an evaluated result. The
deck itself is compiled by Lean. Now let me do the less toy version live.”
LIVE — prove job one first
record → function → Except → Array → typed scene props → JSON → SVG
3 × 3 → 4 × 3
success → explicit error
9 samples → 600 multivectors
Switch to Cursor · OrdinaryProgrammingDemo.lean
2:35-9:45. Switch to Cursor.
In OrdinaryProgrammingDemo.lean, show tinyGrid, swirlField, and
sampleCount.
Put the cursor on the successful #eval: Except.ok 9.
Edit only xCount := 3 to xCount := 4; show Except.ok 12.
Show the final invalid-grid command and its explicit error.
Switch to MultivectorFieldDemo.lean, click #html, toggle grade 2 off/on,
play/pause, drag the empty background once, and reset.
Use the plain explanation: number, arrow, oriented plane, oriented volume.
Say once that these are Float computations, not proved real-number facts.
After the visual, return to this deck and advance once.
One program, three reusable boundaries
F_0(p)=v(p)+p\,v(p)+\tau(p)I
F_\theta(p)=R_\theta F_0(p)\operatorname{reverse}(R_\theta)
Lean owns positions, products, coefficients, 24 frames, validationthe view owns projection, glyph geometry, interaction, SVG
9:45-10:45.
Say: “The basic file imports only the renderer-neutral field library. The
visual opts into a separate InfoView library. The JavaScript does not perform a
Clifford product, rotate a coefficient, resample, or interpolate a frame.”
Explain only one algebraic fact: p*v contributes scalar and oriented-plane
parts. The vector term gives arrows; the pseudoscalar term gives halos.
Not “Haskell bad”
Haskell's strengths held up.
Lean's niche is not “nicer functional syntax.”
Lean is an ordinary languagewhose second job is not ordinary.
program → test → specification → proof → editor tool <br>
browser demo · presenter tutorial · one-screen cue card
10:45-12:00.
Close: “So my claim is narrower than ‘Lean beats Haskell at everything,’ and I
think more interesting. Lean is better differentiated. You can start with
records, functions, arrays, errors, and a UI; then move selected invariants into
dependent types and proofs without changing languages. That gives Lean a
reason to exist even when Python is easy to generate.”
Repeat the boundary: tonight's visual is numerical runtime evidence, not a
formal proof. Stop at 12:00 and use the remaining three minutes for questions.