img {border-style: groove;} Someone recently told me a project isn’t real until you do a retrospective, so I think it’s time to do one for Let’s Prove Leftpad. Short explanation: it’s a repository of proofs of leftpad, in different proof systems. Long explanation: the rest of this post. Background I’m into formal methods, the discipline of proving software correct. Consider the following contrived code: def add(x: int, y: int): int { if(x == 12976 && y == 14867) { return x - y; } re...
