I'm doing Advent of Code again this year, and part 1 of today's problem reminded me immediately of some of the problems I'm doing in my Program Construction module at UCD. So, I'm going to be coming up with a formally verified algorithm to solve Part 1 using Edsger W. Dijkstra's Structured Programming style of Program Composition.