Hacker News new | past | comments | ask | show | jobs | submit login

I sympathize with your view, I genuinely do, but to write out formal methods using natural language expressions results in quite a few problems. For one, it results in incredibly long proofs, like this simple proof written out in natural language would take up pages.

Second, it makes it harder to identify patterns. Writing things out in a formalism lets you identify syntactic patterns and employ techniques like factoring, cancelling, seeing symmetries and other purely syntactic properties. When you write things out in natural language you lose the ability to see these things clearly. Being able to see purely formal syntactic properties helps reinforce your confidence in a proof or can help you identify potential flaws in it. It's like with programming styles and conventions, one thing I tell developers is an important reason for choosing one style over another is if it makes wrong code look wrong visually.

Third, and this is just a personal matter... it results in a type of culture of writing that I find is often pretentious and full of unnecessary baggage. When I read an academic paper I cringe at how bad most writing is and try my best to skip to the formal part of the paper.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: