That is why Iverson invented APL. As a notation to get rid of all those inconsistencies in math notation. And for years he taught math classes with APL on the blackboard without computers.

whether he succeeded, is debatable. But APL is definitely powerful, succinct and "regular".

In APL you don't infer the operation from the types at all. × is elementwise, +.× is inner product /always/, on scalars, vectors, matrices, whatever. The glyph tells you what happens. Nothing is bold, nothing is inferred, nothing depends on what your professor assumed you'd absorbed.

I've been trying to get into Iversonian languages myself with the book: Calculous on J

My favorite moment of this kind was when the teacher said 'Ok, and for the rest of the course we will look at a completely different problem', and the equation he wrote down was exactly the same as before. Except that the letters referred to vectors/matrices now.

Aye.

A decade or so ago I wondered if the reason maths was hard was the names being optimised for writing by hand. Everything's single letters if they can get away with it, so when mathematicians run out of Latin alphabet, they use Greek, bold, etc.

Even integration's ∫ is a fancy elongated s.

CS version would be e.g. integral(function=some_named_function, from=a, to=b, with_respect_to=argument_of_function), which may be longer, but is less opaque, especially when you get in so deep there's 3 other people in the world who've looked into this specific problem and you had to invent your own operations.

But that's all an outsider's perspective. I stopped with two A-levels in maths and further maths.

I was reading about Tao's efforts to get more people to use Lean and apparently a big roadblock for people is that Lean uses very specific static typing.

e.g. to use a very simple example on a white board "3" is "overloaded" as:

- the integer 3

- the rational number 3

- the whole number 3

- etc

When you write a proof in Lean, you have to specify the the type of "3" you mean.

Having using Python/Perl and Java over the years, I get that some math folks found handling this daunting or at a minimum friction to getting into using Lean.

LLMs seem to have been a big help here just for the "translate my math notation into a proof" feature.

Sometimes I wonder if mathematics would have been significantly more improved if they hadn't insisted on notating their variables as single letters and also indicated variable types out-of-line (or at all)...

but then I take a look at literally anything the Haskell people do and realize that it probably wouldn't have helped.

For what it's worth, it's not a problem with multiple kinds of multiplication (multiplication by a scalar can be viewed as multiplication by a specific kind of matrix), but with the idea that one can cancel in a multiplication. Since you can't cancel in matrix multiplication, you run into unexpected trouble when you try to do so, even if that's the only multiplication in sight. (In fact, you can't cancel in scalar multiplication either unless you've checked that you aren't multiplying by 0 …. Also, I'll note that surely no young mathematician has encountered the P = NP problem without thinking for a sophomoric moment that the solution is N = 1.)

>For example, in my quantum class the teacher wrote "H Psi = E Psi" on the board, we all laughed, "just cancel the psi" but it turns out one was a multiplcation and the other was a matrix multiplication (operator) and so we had to learn all new nomenclature.

This is one of the great things about Lean becoming used for more and more mathematics: understanding exactly how an operator/function is defined is just an IDE click or few away. It completely removes the ambiguity present in hand-written proofs, although it still can require a lot of reading to actually meaningfully understand the definitions.