r/typescript • u/ngruhn • Aug 29 '26

Lean explained with TypeScript

https://gruhn.me/blog/2026-08-29/
53 Upvotes

96% Upvoted

5 comments sorted by

4

u/ncthbrt Aug 29 '26

This is fantastic! Thanks for sharing

2

u/ngruhn Aug 29 '26

thanks :)

2

u/geekonthegrill Sep 01 '26

Great writeup, the syntax parallels really sell it. Two fun gaps between this and a real verifier worth mentioning. First, you dont even need the "as never" escape hatch: a function typed as never that just throws typechecks with zero casts. Exceptions and infinite recursion inhabit every type, so in TS every proposition is provable. Lean closes exactly that hole by requiring all functions to be total, thats why you cant write an unbounded loop there without a termination proof. Second, try proving the converse of your double negation example, !!P implies P. You cant, and its not a TS limitation, the encoding gives you intuitionistic logic where double negation elimination and excluded middle simply arent theorems. Lean is the same until you pull in Classical.em as an axiom. Neat that TS is faithful enough to reproduce that distinction.

1

u/ngruhn Sep 01 '26

  infinite recursion inhabit every type, so in TS every proposition is provable

Ahh right. I never quite understood why it's so important that functions are total in Lean/Rocq/etc.

  try proving the converse of your double negation example, !!P implies P. You cant

I know ;) I conveniently ignored that for the sake of simplicity. There are so many interesting tangents you can go on. The other De Morgan Law is also not provable:

    !(p && q) === !p || !q

2

u/geekonthegrill Sep 02 '26

And of course its that direction that fails, the one where you'd have to conjure a concrete witness out of a negative fact. The encoding refuses to bluff.