Thread by @jjcarett2

Note that floating point isn't math. It's a weird method of approximation that was invented because doing it 'right' was too slow on "early" computers. People are figuring out that many of the underlying design compromises might have been exactly right then, but not so now.

Instead, pick a decent textbook on Calculus. I'm partial to Spivak's brilliant tome, but Stewart's will do too, if you insist. Then try to use a computer to help you.
First most current programming languages will not be helpful at all, at least not without a huge amount of work.

So you try a CAS (Maple or Mathematica will be fine, SageMath not as much, it doesn't like Calculus). You get a lot farther. At least you can *represent* many of the things in your textbook. Often, do more (esp. for visualization). Win?

Nope. Because many of the exercises ask you to prove stuff. And you realize that these systems can't help at all. [Not for Calculus]. So you turn to theorem provers. The automated ones are useless - they don't do calculus. The interactive ones?

Well, they are a lot of work. But you persevere. Coq, Agda, Idris, Lean, cool as they all are, fall to the wayside - they don't really do 'reals' nicely. HOL Light and Isabelle survive, and they let you indeed do many proofs rather easily. Win?

Nope. Because all of the nice computations that the CAS allowed you to do are now *gone*. All those algorithms (which required 100s of person-years to create), poof.

So you ask yourself -- why is this? Well, in part, it is because efficient computation and correct proofs actually live in different parts of the design space of 'mathematics'. But, wait a second, you say, what about Curry-Howard? Glad you asked!

The correspondence between logic and the lambda calculus does not in fact say anything about efficiency. And, more deeply, it also does not speak about the much bigger problem: intension versus extension. plato.stanford.edu/entries/logic-…

The really deep problem is that 'symbolic computation' is about computation on syntax (aka intension) that is meant to reflect truths valid in the intended model (i.e. extensionally). Whereas theorems are meant to be proved directly in a model (or class thereof).

There is a "representation" step that lies between. For human mathematics, it can be blurred (and almost always is), without much harm. Basically human mathematicians are taught 'good taste' early on, and never write down 'junk' (although see mathoverflow.net/questions/9082…)

But when you try to teach math to a computer, this representation step becomes extremely visible, and a huge burden. Computers don't know when a piece of syntax is meaningful (or meaningless). It's just a bunch of bits as far as it's concerned.

And the real kicker is that many of the (constructive) theorems of calculus can be read as rewrite rules. When your input is meaningful, they work. When your input is meaningless, they often *still* can be used, to give 'results'.

Sometimes these results have non-standard interpretations and can be given meaning (like Schwartz did to rehabilitate the Dirac Delta, and Ecalle for divergent series). A CAS will most happily tell you that 1/(1/(x-x)) is 0. Ok, so 1/0 = infinity, sure, but 1/infinity=0?

And that's just the start of trouble.

But it all comes down to one deep-yet-invisible dichotomy of mathematics:
1. symbolic computation is about syntax
2. proof is about semantics

Teaching math to a computer requires the teacher to understand *that* first!