Lean's Metaprogramming - Harry Goldstein's Talk

How will things play out?