[HN Gopher] Formally verifying Advent of Code using Dijkstra's p...
       ___________________________________________________________________
        
       Formally verifying Advent of Code using Dijkstra's program
       construction
        
       Author : seafoamteal
       Score  : 25 points
       Date   : 2025-12-03 18:39 UTC (4 hours ago)
        
 (HTM) web link (haripm.com)
 (TXT) w3m dump (haripm.com)
        
       | Joker_vD wrote:
       | That's a lot of manual effort to save just a tiny bit of
       | thinking. The first digit is the largest digit among the first
       | N-1 digits. The second digit is the largest digit to the right of
       | the first digit up to and including the Nth digit. That's it.
        
         | seafoamteal wrote:
         | Hi! Yes, I talk about this a little bit at the end and I solve
         | Part 2 the normal way. This is a toy example that I did for
         | fun. The objective was to introduce people to Program
         | Construction and show how you can use formal methods to derive
         | correct programs. Whether the juice is worth the squeeze is a
         | judgement call that you make depending on how critical the
         | software you are writing is.
        
       ___________________________________________________________________
       (page generated 2025-12-03 23:01 UTC)