Hacker News Reader

Comment by xiaq | Hacker News Reader

True, but the point is that in principle you can write very detailed, fully formal proofs, in exactly the same manner programs are written. The rest of my comment then discusses why it is not written that way.

Doing formal proofs manually is like writing turing machine instructions. Computer-assisted proving gives you higher level tools, but apparently it is still not powerful enough to be accepted in mainstream. And unlike programming where you get stuck if you haven't invented higher level languages, mathematicians have the widely accepted tool of "it trivially follows". Bourbaki might disagree, though.

View on HN

That's a very illuminating analogy.

Users of high-level languages, typically do not think about what the compiler is doing, and if in fact they do not know the compiler action--often the only way to find out is by reading the compilers source code.

This is akin to looking a math paper seeing "it trivially follows..." and your only recourse to find out why it so trivially follows is to get a mathematics degree.

There is still a key difference.

With programming the information is always there. If you don't understand a higher level language but do understand the language in which the compiler is implemented, you can always read the compiler.

The "it trivially follows", the information is simply missing. Gaining a mathematics degree will often give you the intellectual power of finding the missing pieces yourself, but the only sure way is to ask the authors themselves.

At least in programming it's possible to step into a function and/or work at multiple levels of abstraction.

Getting a math degree just to be able to fill in the gaps created where 'it trivially follows' is equivalent to being required to memorize the API for a framework because clearly defined documentation is hidden behind a paywall.

so called 'intellectual power' has little to do with it. What you're describing is familiarity with navigating a minefield of poorly structured information and tapping a academia (ie at a very high cost of entry) for 'special access' to resources that bridge the gaps.

Of software development suffered from the same informational constraints and lack of innovation, we'd still be playing pong.

> ... because clearly defined documentation is hidden behind a paywall.

Hmm you are from US aren't you? :)

Well said. Memorizing the API is fundamental to success in most branches of math - but this erects a barrier that a lot of able individuals are unable to cross. I've always thought this was a problem but I almost never hear of anybody complaining about this so I figured it was just me. Languishing in the established system is usually interpreted as "sour grapes".

It strikes me as a collective means for mathematicians to reduce entry into their field and thus to increase their own salaries. Maybe you don't have to get a "math license" to practice math, but you have to somehow acquire a huge body of knowledge that is almost never spelled out fully in the mathematics literature. This will prevent many people from becoming mathematicians and thus make math a more exclusive and lucrative endeavor.

To be cynical about it.

I guess that's not much different from most fields' use of specialized vocabulary, etc. There are many informal methods of dissuading people from competing in your own little corner of the labor market.

Reply on news.ycombinator.com