> If you have a goal of being able to confidently reason about your code, such as to be confident it won't go "wrong", then making it more math like would seem to make a lot of sense.

Is it easier to reason about a 10,000-line-long math proof, or a 10,000-line-long program? I'm not sure that the math is actually easier.

Is it easier to write a fully-correct 10,000-line-long math proof, or a 10,000-line-long program? Again, I'm not sure that the math is actually easier.

Is it easier to write a formal prover for the math? Almost certainly. And maybe, with a formal prover, writing the correct math is easier...