= 27d567bc2d48d9f40e9ccc20ea370b15)
AlephNeil comments on Making Reasoning Obviously Locally Correct - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (23)
If the cost of having written down an incorrect proof is much higher than the cost of burning up a lot of time then sure, making each step rigorous will be worthwhile. In mathematics, however, that generally isn't the case. No-one writes fully rigorous proofs - and occasionally someone spots an error in a published proof. Progress is much faster this way.
In programming, the costs and benefits may of course be totally different, depending on the project.
The example I made of being rigorous was excessively verbose because I was trying to demonstrate rigor to a general audience without making a lot of assumptions about background information. Mathematicians communicating with other mathematician can rely on a common knowledge of theorems and notations to write more concisely. They can factor a quadratic expression in one easily verifiable step. They do use "division", though they can drop down a layer of abstraction and explain it in terms of multiplicative inverses, and either way, they know they have to make sure the divisor is not zero.