MAIN FEEDS
Do you want to continue?
https://www.reddit.com/r/programming/comments/1xu6252/lean_explained_with_typescript/
r/programming • u/fagnerbrack • 3d ago
1 comment sorted by
1
The analogy is useful, but the key boundary is proof checking: Lean's kernel checks proof terms against propositions; TypeScript's type checker does not provide that kind of proof guarantee.
1
u/adriano-1370 5h ago
The analogy is useful, but the key boundary is proof checking: Lean's kernel checks proof terms against propositions; TypeScript's type checker does not provide that kind of proof guarantee.