Metaprograms and Proofs: Macros in Lean 4 (twelfth RacketCon)

A core feature of the Lean 4 programming language and theorem prover is an expressive macro system, taking heavy inspiration from Racket. In this talk, we give an overview of macros in Lean and discuss the ideas we took from Racket as well as the problems we decided to solve in a different way. In particular, we talk about recent work on typed macros that prevent many common mistakes by Lean macro authors.
Bio: Sebastian is a PhD student at Karlsruhe Institute of Technology, Germany, and a Lean core developer. He enjoys both working on the user-facing frontend of the system as well as on the code generation backend to make users and binaries go fast.

[@leswine1582]

n8ce