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.
Related
LangChainAI
Note ·
LangChainAI, is a framework (python library, and also javascript), for developing application powered by llm. Be…
Interesting Programming Languages
Note ·
an opinionated collection of programming languages.
Programming
Note ·
Notes on Programming as a practice. Collect notes about programming language at the "language" level without getting…
C Programming Langauge
Note ·
The thing after A, and B.
LLM
Note ·
large language models
Jetbrains
Note ·
Junie "The coding agent that works with any model you choose." curl -fsSL https://junie.jetbrains.com/install.sh | bash…