I think he was trying to show that the TLA+ approach led to easier proofs of the base case and inductive case. I don't think he's arguing that your gcd program is bad. That's what I'd use. But TLA+ might be a good tool to break out when you need to have a solid proof that the code you wrote will always end up getting you the right answer. We probably don't need it for side projects, but it's nice to know that AWS has some proofs around that the services I use there can't end up in an inconsistent state as a result of any coding logic.