When I was writing my proposal to get into a PhD program, I had to do a crash course in formally verified applications. The focus of the program is actually in

When I was writing my proposal to get into a PhD program, I had to do a crash course in formally verified applications. The focus of the program is actually in Isabelle, but Coq is similar enough (in a hand-wavey kind of way) to where it was relevant to what I was writing about, and I stumbled across a few formally verified things with Coq. I became slightly obsessed with CompCert, but it felt like a "real" program that was utilizing proper formal verification techniques. It seemed so cool to me that there can be (to some extent), and "objectively correct" version of a C compiler. I still think it's very cool; I wish people would geek out about this stuff as much as I would sometimes.