This blog has been on my to-do list for a while now. It has been a month since I went to IndiaFOSS, and I could finally finish it thanks to my retreat at the Isha Foundation in Coimbatore, and to two days of an Instagram-free life that let me collect all my thoughts and put them into a document in less than a day.
Writing invariants gets treated as an art form, which is a polite way of saying nobody can explain how they do it. “Art is long and life is short,” said Hippocrates, a man who never had to read a 2,000-word post on formal methods. So I’ve tried to keep this one short.
A couple of weeks ago I travelled to Bangalore for a hackathon at the Indian Institute of Science, organised by Prof. Siddharth Gadgilreference for Prof. Siddharth GadgilProf. Siddharth Gadgilmath.iisc.ac.in/~gadgil and Emergence AI. The structure of the hackathon was: spend the first couple of days getting taught Lean4reference for Lean4Lean4lean-lang.org by Prof. Siddharth Gadgil and Prof. Prathamesh T. V. H.reference for Prof. Prathamesh T. V. H.Prof. Prathamesh T. V. H.krea.edu.in/sias/dr-t-v-h-prathamesh, then disappear into a cave for a weekreference for cave for a weekcave for a weekyoutube.com/watch and emerge with a project. The judges were Anand Rao Tadipatrireference for Anand Rao TadipatriAnand Rao Tadipatridl.acm.org/profile/99661086046 and Sidharth Bhatreference for Sidharth BhatSidharth Bhatgrosser.science/team/bhat; both PhD students in mathematics at the University of Cambridge.