Harry Goldstein

Harry Goldstein, a researcher in software testing and Lean 4 metaprogramming, shares his insights with Richard Feldman. They explore Lean 4's compile-time metaprogramming, particularly its ability to enhance IDEs in real-time. Harry discusses ProofWidgets, properties of totality, and the balance between trusted cores and flexible metaprogramming. They touch on security concerns with metaprogramming and the implications of property-based testing. The conversation also draws interesting parallels between Lean and Smalltalk's dynamic capabilities.