But that big paragraph is the natural language version of the formal proof. It's less strict and has more helpful concepts than any programming language in the world. It's that big because there actually are a lot of details needed for the proof. For instance it's not necessarily true that x = y = z means x = z, I need to provide a proof of that (transitivity of equality), it's not necessarily true that just because x = 3^a 5^b doesn't mean x isn't also 2 * <some other prime factorization>, I need a proof of that. Etc. Unless the computer is smart enough to do all that work for me. In which case the language isn't just nicer, it's also got an automated theorem prover.
Something like lean isn't assembly, it's a full fledged language with abstractions, better IDE support than I've seen for any "real" programming language, the ability to program new "tactics" (methods of proof), and so on. I'm not trying to prove things in raw logic in it. The thing is I don't want to be trying to prove some of these things at all, I want the reader (the compiler) to just go ahead and supply their own proof.
Something like lean isn't assembly, it's a full fledged language with abstractions, better IDE support than I've seen for any "real" programming language, the ability to program new "tactics" (methods of proof), and so on. I'm not trying to prove things in raw logic in it. The thing is I don't want to be trying to prove some of these things at all, I want the reader (the compiler) to just go ahead and supply their own proof.