[I'm doing](https://tangled.org/haripm.com/aoc_2025) [Advent of Code](https://adventofcode.com) again this year, and part 1 of [today's problem](https://adventofcode.com/2025/day/3) reminded me immediately of some of the problems I'm doing in my [Program Construction](https://ucd.ie/modules/COMP30060) 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.