Advent of Code in Coq
Series status: Suspended
First post in 2020, last post in 2021
In this series, I apply the Coq proof assistant to formalize solutions to the puzzles to Advent of Code 2020. That is, I try to solve the problem, and formally prove that the solution is correct.
-
Day 1
3515 words, about 17 minutes to read.
The first puzzle of this year’s Advent of Code was quite simple, which gave me a thought: “Hey, this feels within reach for me to formally verify! ...
-
Day 8
8609 words, about 41 minutes to read.
Huh? We’re on day 8? What happened to days 2 through 7? Well, for the most part, I didn’t think they were that interesting from the Coq point of view. ...