I’m a PhD student in programming languages who sometimes uses Coq to prove properties for my research.