Developer of katydid, gogoprotobuf, goderive, gographviz, erlfmt and lots of other even more embarrassing open source projects. Now I am learning how to prove code is correct using Coq and Lean.