| Hello there. I'm the author of this repo. Not as much has been going on in that project as I would have liked. It certainly doesn't help that: - The standard library is actually quite poor. A lot of basic functions must be implemented from scratch, and then you'll also want to write proofs about them. - I had to reinvent IO in Coq. - Most AOC problems are actually not that well-suited for formal verification. (It's certainly no fault of the AOC organizer!) In particular, a lot of them basically ask you to simulate some system which doesn't have particularly interesting properties, so the implementation itself is often the best specification of the problem, and the main point of using a language like Coq is lost. I did find some interesting problems though. For example, day 5 was a simple rewriting system and the question was to find the normal form of some starting string. Well, who's to say that the answer is unique? In this case it's easy enough to convince oneself that the given system actually is confluent, but I set out to prove it formally (and (re)learned a few things about rewriting systems on the way). (c.f., Confluent_react_steps, react_steps_injective, in day_05_common.v) |