What I understood after studying CS for over 10 years at a few universities regularly ranked highly at ACM ICPC is that math is unnecessarily obfuscated to most people. There is even an excellent book "Concrete Mathematics" from Stanford that tries to bring fun back to math instead of drying people with some formal stuff without explaining how people over the centuries got to that structure.
I honestly believe math language is seriously outdated. It's like using COBOL to express everything. Yes, you can do that, but would you really want to given a choice? The most trivial things are so insanely complicated in math it's unbelievable (try to describe geometrical objects with the current math formal language if you do computer vision), yet there is very little work on developing better formal language of math. It's like with Turing machines and the complexity theory - who is going to move around a tape in the real world besides some specialized biological systems, not mentioning magical 'oracles'? Those abstractions were useful in their day, brought their fruits, but why do we still stick to them and just increase the gulf between more and more closed-unto-itself-theory and reality? Yes, it's great some theory is super cool but what do we do when we find in 20-30 years that the set of objects satisfying this omnipotent theory is empty? And when somebody like Mochizuki invents their own formal language to solve some cool problem like ABC conjecture, we all hate him, refusing to read the proof because it doesn't follow our outdated formal ways...
I agree strongly that math is poorly taught most places and that Concrete Mathematics does an admirable job of teaching math in a way that gets to the beauty of it. Oddly enough, it wasn't until I threw myself into more advanced mathematics that I started to see the fun in it. I absolutely hated learning calculus and linear algebra even though I could do it well. It just seemed so boring. I don't have a good solution to how to make things better, however, the mathematician Paul Lockhart has given this a lot of thought.
All that said, I think there are a number of misconceptions here.
First, mathematicians invent new languages all the time. That's the point of definitions, otherwise we'd be using sets to describe everything. The problem is, you first have to understand the concept well in order to apply suitable definitions. Think probability before Kolmogorov.
Second, Turing machines are a formalism to introduce you to the theory of computation because they are the simplest (or close to it) thing that can compute in the current sense of the word. Once you learn how TMs work, pretty much everyone just accepts them as a given and deals at a higher level.
Third people are trying to read Mochizuki's proof, but it is very hard. He basically invented his own way of doing things and so to understand his proof you first need to understand his methods. It's understandable that professional mathematicians with their own careers and areas of research find it hard to read the ~1000 pages of dense mathematics (proof + prior papers) to understand what is going on. Most people probably haven't read 1000 pages of math in their life, and it takes a while to come to terms with it no matter how smart you are.
This is what drew me to CS over math. I enjoy describing things with code or pseudo code, not difficult to understand equations and math symbols. Also, it is much easier to see the practicality of an equation when presented in code form.
"Computer science" can mean many different things, but theoretical CS is largely considered a branch of mathematics. While there is some 'code', it has all of the same formalisms, equations and proofs. CS papers can be just as inaccessible as other types of math, if not more so.
After I read SICP and HtDP I started retaking math I had forgotten but writing out the equations in Scheme to further grasp the language. At first doing Spivaks Calculus in this method took a long time but now I can write formulas and basic proofs just as fast in a programming language as I can with a pencil.
I skimmed SICM (Structural Interpretation Of Classical Mechanics) just to get an idea of how they represented Langrange equations in Scheme and went from there.
This is something I like doing. Something I keep meaning to do is take it further and write my proofs in a proof checking language, or at least write "unit tests" for my proofs with one (interleaved with the natural language proof with org-mode!), but they all seemed pretty unwieldy. Has anyone tried this with any success?
For your analogy with Turing machines, do you have a better mathematical model of a computer? Nobody works directly with the TM model when they're doing theoretical CS anyway, they just describe the algorithm and everyone understands that if you really really wanted to you could work it down to a TM.
The same is true of mathematics. It might be hard to get everything precise, but that's not the point of mathematics. Nor is the point to be close to reality.
> All you have to do is demonstrate that TMs can be simulated in JavaScript, and that's fairly easy to do since TMs are so bare-bones.
Actually I think this is fairly non-trivial. Sure you could make a "compiler" that compiles a JavaScript interpreter down to a Turing machine, but you would almost certainly not understand the generated states and transitions.
A more elegant model of computation is the lambda calculus. It's also very bare-bones, but it's easy to imagine writing real programs in it. Functional programming languages, at their core, are just lambda calculi with some syntactic sugar.
It's practical, but it's also a good foundational model. It's easy to reason about, due in part to the fact that it models familiar math (partial functions).
There are far simpler models for formal verification than Turing machines, e.g. Smullyan's top-down tableaux method - you make a simple functional snippet and immediately verify it using mostly general induction and easy-to-understand verification steps that can be almost automated. Going all the way to the Turing level would kill you time-wise to get to anything useful (even preparing description of your JavaScript machine in Turing terms) - Turing machine has infinite time available, you don't.
Not to mention there are some issues with formal logic that might cause you problems (hint: why do medical doctors use counter-factuals and not mathematical logic?)
"Beware of bugs in the above code; I have only proved it correct, not tried it" -- Donald E. Knuth
I tried going through "Concrete Mathematics," but I could only do a handful of the problems in the first chapter after trying for a couple weeks. I'm not sure why it seems so hard to me -- I've taken a couple "higher math" courses and am generally considered "pretty good" at math. Perhaps I'm better at bullshit than math...
I honestly believe math language is seriously outdated. It's like using COBOL to express everything. Yes, you can do that, but would you really want to given a choice? The most trivial things are so insanely complicated in math it's unbelievable (try to describe geometrical objects with the current math formal language if you do computer vision), yet there is very little work on developing better formal language of math. It's like with Turing machines and the complexity theory - who is going to move around a tape in the real world besides some specialized biological systems, not mentioning magical 'oracles'? Those abstractions were useful in their day, brought their fruits, but why do we still stick to them and just increase the gulf between more and more closed-unto-itself-theory and reality? Yes, it's great some theory is super cool but what do we do when we find in 20-30 years that the set of objects satisfying this omnipotent theory is empty? And when somebody like Mochizuki invents their own formal language to solve some cool problem like ABC conjecture, we all hate him, refusing to read the proof because it doesn't follow our outdated formal ways...