I agree. I always felt that if math theorems were presented in a programming language, they would be way more understandable (especially if the good practices are respected: meaningful variable names, etc).
Mathematicians love to talk about rigor, but when it comes down to write their ideas, they often have little enough of it.
I always felt that if math theorems were presented in a programming language, they would be way more understandable ….
Find out empirically! Look at theorems in some formal methods/programming languages papers and their corresponding mechanizations and see which you find more understandable. (Actually, it might be better to start with something like Software Foundations to get a gentler introduction to a programming language used for this sort of thing -- http://www.cis.upenn.edu/~bcpierce/sf/ )
Hard to do, the one you will look at second will always be at an advantage. So you'd have to select two theorems of "equivalent difficulty", which is not easy. Also you need to select hard to understand theorems, else you'll understand both the representations easily anyway.
Mathematicians love to talk about rigor, but when it comes down to write their ideas, they often have little enough of it.