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.