I'll use this opportunity to recommend Conrad Wolfram's "The Math(s) Fix" that outlines his Computer-based Math approach. In this book he asks (and answers) what would school look like if we taught mathematics as if computers exist.
Math always felt very random and arbitrary to me. Especially the fact that proofs are essentially just prosa and people believe in them or they don't. And that's why we ended up with proofs that essentially were correct but still had flaws and errors in them for a long time. Or proofs that actually turned out to be wrong in the end.
And when you are done, the least obvious steps (for your reader) will be hidden in a forest of obvious steps. Suppose that you want to communicate to someone how to get to B from A. You don't tell them "lift your foot in this manner, then lift your other foot in this other manner, go a little left when you see this small obstacle", etc... you assume that they have competence at navigating commonplace obstacles, and give just the directions that they should take at intersections.
To me, the example is rather to tell them get into the car then press the button and turn the wheel like this and you'll reach your destination. But they won't understand the car and I think they should, because at some point the need to, unless they never dig deeper - but then maybe we don't need to teach those theoretical things from the beginning.
Well, it does depend on the audience you're writing for. So research math doesn't do that, whereas first-year undergrad math makes an effort to. I think it's essential for first-year math programs to have a course where you redevelop basic induction, natural numbers, addition, etc. from first-order logic and rules of inference and ZFC, which I don't think is true everywhere. And there should be an aspect of it that's about converting that formal proof to informal proof given some assumptions about the reader. Beyond this, it starts to get tedious.
People often write equations out in full and marvel at the ludicrous clunkiness of it all. Usually because they expect that will help them understand a concept. That doesn't work.
The notation often suggests a manner of thinking about an idea that is more useful than seeing the idea spelled out.
Of course you probably should have spent some time peering into the blackbox of notation and physicists are probably most notorious for not caring to.
The notation often suggests a manner of thinking about an idea that most won't be able to see in the expanded notations.
As such those familiar with the field often abstract away the minutia.
I always heard a rather unfair terse statement about science. If you have to read the articles introduction section, you probably shouldn't be reading the article. That's wildly unfair but does reflect that academia is mostly concerned with academics in the same field.
Don't get me wrong, there are all sorts of disastrous notations in math that should be fixed. Those just aren't them.
Anyway, the computer science version with types is gonna be so obtuse that you're gonna wish you had this back.
The people who haven't learned it and are complaining about how daunting it seems can certainly have opinions but their opinions aren't very useful and interesting.
For example, it's not clear that you've considered that the people you're replying to have learned the subject matter and are reflecting on what would have made the process easier for them.
In general my reaction is a sort of counter-reaction to a HN pattern that I don't like. Every HN post has someone say "this is so stupid" on it, about something (all kinds of things usually). I really hate that. So my flinch response is to say "this objection is also stupid". Not helpful and just as bad as what I'm criticizing, really. I regret it.
Somewhat kooky afterthought: I don't like those initial critical nitpicky reactions because they sort of.. encode.... a rather unlikeable philosophy that is always in subtext here, which is that everything can be solved by building something, or doing something 'right', and regular human effort to solve human problems, with its human flaws, is worthy of scorn. Never cared for that. I think that's why I react negatively to it. Like in this case: those notations are actually good for a bunch of reasons. Strongly typing it? Try that for twenty minutes and you'll see why it's gonna be worse (I mean... probably. maybe I'm wrong! glad to learn). Or maybe every blog post define its terms more carefully for people who didn't learn from school? I dunno, I had a blog and tried that and it makes the posts crap, filled with meticulous definitions. At some point you just have to assume some things about your audience, and let them google what they don't know.
Derivatives are a bit of a weird case because some really intuitive and useful sub-domains only really need the 1-2 derivatives in time. So, hitting them with the whole (dy/dx)^(N) is overkill.
That’s nothing. Study real analysis long enough to investigate sequence spaces and you’re looking at sequences of sequences. The notation for those will often use subscripts and superscripts as indices at the same time! But generally you’re not dealing with derivatives or exponents at the time so it’s not too bad.
Mathematics, though, is a language developed by academics for academics, who will spend a long time iterating through variations on the same pattern. When you're years into your post-grad, looking at the same tiny slice of mathematics over and over again, it's obvious what f^(n) means - you've probably written that and thought about it thousands of times - but yeah, it does suck for outsiders.
Given the exorbitant cost of education (in the US), I think this is a reasonable desire or expectation for a student to have.
Often I'll see some maths equation in a paper or blog post or whatever that I want to use in software, but I don't understand the notation and so I can't use it without spending god knows how long learning all the context first.
All language suffers from this. Without context (assumed by the reader, provided fully or at least referenced by the writer) all arbitrary expressions are impossible to parse. Tell me what this means:
map f xs
Math isn't any different here, don't try to parse arbitrary expressions until you've identified the context. Maybe a fool used notation foolishly, maybe an adversarial mathematician used notation to obfuscate and has, hidden away in their diary, a key that explains it all. But most of the time the context will be provided directly or indirectly. The notation will be explained in the text or the text will be in a field with notational conventions that the reader is expected to know. Same with code, same with every other human language.
[1] https://hackage.haskell.org/package/base-4.17.0.0/docs/Data-...
> If any of those symbols are undefined, the editor or compiler will tell me.
I'm pretty sure every single language in the world will tell me that statement in isolation will not compile.
We are either in violent agreement or you are failing to actually convey your meaning.
To take a step back: The original commenter complained about not being able to parse arbitrary expressions. I responded by pointing out that that's not a math specific thing, and that every language has this problem if there is no context. My overall point being that with context that "arbitrary" math expression would become less arbitrary as the context provides meaning which permits parsing. Since they seemed to be a programmer (or have some familiarity with it, asking for a strongly typed language) I provided an expression you might find in some program, and presented it without any context, that was intended as an analogy to their situation with math. Again, trying to emphasize that you need context to get meaning.
You seem to be agreeing with me (you need context for the expression to have any meaning), but your comment itself comes off as argumentative. So what's your disagreement with my point?
A type system is itself a programming language. If it is going to implement complex enough logic, it will be Turing complete. It does not magically become clearer simply because it ideas have been expressed in a type system. For an amusing demonstration, read through https://aphyr.com/posts/342-typing-the-technical-interview. That is a working program that solves the 8 queens problem entirely in Haskell's type system.
And the type systems that you are used to are simpler in part because they are NOT Turing complete. This limits what you can say in them. In this case, for example, the author was unable to express higher derivatives as types.
Now perhaps your desire is for unambiguous machine-checkable logic? If so then I highly recommend learning something like https://coq.inria.fr/. It is a worthwhile enterprise, and there are serious mathematicians who say that it, or something like it, should be implemented for all of math. However one of the objections to it is that it is harder to express and understand yourself in such systems. So unambiguous machine-checkability is a win, but not necessarily the one you thought it was.
And then we come to the real issue. Are you optimizing for use, or for the person who doesn't understand the subject? It is literally impossible to think about complex things without a concise notation. The actual notation that we have has a lot of history and rough spots. But verbosity impedes comprehension. So what makes life easy for the novice and expert are exactly opposite. Also most of the use of the material is by experts, who are also who the notation is designed to be most helpful for. However even for students it helps. So much so that learning the notation generally pays off within a course or two. That is, learning the same ideas WITHOUT the notation would have been harder than learning both notation and ideas. So notation merely creates an obvious barrier, but then helps with the real one.
I know you don't believe me. You've told others that it is about what works best for you. But with all due respect, you can't have any idea what actually works best for you until you've actually mastered a sufficient amount of the subject. Which you apparently haven't. Until then you are best off believing people who HAVE mastered the subject, and have spent sufficient time teaching and tutoring to know where the real barriers to understanding are for students. And everyone I know in that boat, including me, says that the notation helps more than it hurts.
SICM as a textbook is intended to be worked out entirely with a computer.
Why is this true? I think about ∂/∂x, ∂/∂u, and ∂/∂v as higher-order functions that take the same `f` as their argument. What is wrong about this thinking?
[1] https://groups.csail.mit.edu/mac/users/gjs/6946/sicm-html/bo...
Edit: I'm guessing the footnote's reasoning is that on the left hand side, `f` is thought of as `f(x, y)`, and on the right as `f(u(x, y), v(x, y))`.
On the rhs, it very much is not lambda x: f(u(x), v(x)) that the differential operator ∂/∂u (or ∂/∂v) is applied on—because the former would be a function of x.
(I use only x rather than (x,y) for simplicity so you can see where a big problem would lie)
Be aware that the notation in ∂f/∂x = ∂f/∂u ∂u/∂x + ∂f/∂v ∂v/∂x is already very simplified and the actual whole thing would be (in modern notation, as opposed to the one used by SICP):
∂/∂x f0(x) = ∂/∂u f(u(x),v(x)) ∂/∂x u(x) + ∂/∂v f(u,v) ∂/∂x v(x)
Where (as is usual) the (...) denotes function calls, and the ∂/∂x f0 makes a new function, here of x. Note that the function call is done on that new function (this order of precedence is the usual in mathematics)
Also, f0(x) = f(u(x),v(x))
Understanding what exactly is going on where in here is already the basis for fluid dynamics.
Of course, that's the dream. The reality is that people are making very strong efforts at computer proofs, and the languages I've worked with in that space are highly un-ergonomic. On the other side of the chasm, calculus of types is largely relegated to category theory which is its own onion of complexity. To my awareness, Haskell is currently the sweet spot. In the hopes of being proven wrong, I'd guess that we're at least a century away from a Grand Unified Notation that allows a fluid translation between what the mathematician is thinking and how the computer can compute.
[1] https://leanprover.github.io/functional_programming_in_lean/
https://www.ma.imperial.ac.uk/~buzzard/xena/
He started by getting undergraduates to tackle formalising the maths they did in Lean, and his success with this as a didactic tool has spread the idea among quite a lot if mathematicians.
Indeed, once you start to think about formalizing a research-level proof, it brings into focus the sheer number of trivial cases and natural transformations that a standard informal proof in a paper omits.
Math is so full of loosey-goosey context dependent ambiguous notation. It makes it easy to have a very terse expression communicate a powerful idea, but it makes it impossible to just parse an arbitrary expression.
Just as an example, look at the maclauren series as defined in the link. It uses f-dot, f-double-dot, then f^(n), having to note that (n) is the nth derivative rather than exponentiation. You have syntax switching and an ambiguity in the same expression.