an interesting interview with Leonardo de Moura

[Jason E. Aten]

https://www.youtube.com/watch?v=KzdYKeAqWhY

Leonardo de Moura is the Brazilian computer scientist behind

the SMT solver Z3 and the Lean dependently typed programming

language/proof assistant (https://lean-lang.org/ ).

This is a nice introduction to Lean. After the first 30

minutes, it becomes apparent how much more accessible formal

methods are becoming for software verification due to

LLM synergy. I think Lean/proofs will be increasingly relevant to Go,

since assembled concurrent systems are so challenging 

to test well in the large.