Harry Goldstein, professor at the University at Buffalo, explores the programming language Lean as more than just a proof assistant. In this talk, he walks through how Lean enables powerful metaprogramming and live programming features, allowing developers to define new syntax, build interactive widgets, and reshape their development experience directly in the language. This is a look at how a simple language design can support complex workflows and why other languages might want to catch up.

http://antithesis.com/