I would recommend reading the post that Hillel is responding to instead, namely Luke Plant's "Breaking 'provably correct' Leftpad" (https://lukeplant.me.uk/blog/posts/breaking-provably-correct...).