> writing programs is actually equivalent to doing a mathematical proof
Only in the sense that writing in brainfuck is equivalent to writing in Python...
Only in the sense that writing in brainfuck is equivalent to writing in Python...
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.
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.
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.
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.
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.
Hmm you are from US aren't you? :)
> Only in the sense that writing in brainfuck is equivalent to writing in Python...
Actually, in the very concrete sense that a program is a proof for the forumala that is equivalent to its type[0].
[0] https://en.wikipedia.org/wiki/Curry–Howard_correspondence