Similarly, at some point somebody pointed out to me "the reason you're confused is that the bold on that variable means it's a matrix"
Similarly, at some point somebody pointed out to me "the reason you're confused is that the bold on that variable means it's a matrix"
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
https://www.jsoftware.com/help/learning/23.htm is the closest i've found, but wondering if i'm missing something perhaps, Julia?
tyvm
Imagine that instead of being able to use high-level programming languages, you had to write in assembly everywhere, all the time.
That's what software engineers and computer scientists' suggestions of redoing mathematical notation fee like to mathematicians.
These efforts also don't go anywhere because research mathematics moves beyond elementary arithmetic very quickly, and once you're there, "descriptive" notation becomes as incomprehensible as whatever mathematicians use.
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.
Same reason why we write 5-3, not subtract(minuend=five, subtrahend=three).
Interestingly, discrete math feels the most "verbal" of all the subfields of math I've encountered (I haven't gone very deep). I think this is because notation in discrete math is is somehow closer to compressed prose or logic, whereas other forms of math use notation to fill in for long sequences of symbolic manipulation.
Not sure if that makes sense... I'm curious whether anyone else experiences it that way.
People genuinely struggle to think verbally or visually once we extend beyond 3 dimensions and start talking about infinite-dimensional constructs, uncountable sets, and so on...
And math is, as you know, a deep but traversable graph. The traversal inherently requires a familiarity with the nodes you pass through when reaching a foreign or more difficult concept.
However, I'll give you an example. If I read through more complex math that I’m not comfortable with in Sage, I can build an intuition for the structure of the problem more easily than if I view the “raw” notation. In that sense, it is easier to for me to “approach” — but approaching something is very different from fluently using it — and I’m under no illusion that approaching a topic is the same as beginning to understand it.
Again, this is definition-dependent. To me, “approaching” something means beginning to glean how I might one day understand it. E.g. watching a 3B1B video feels like “approaching” a topic. Here we reach the limits of language already :)
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.
but then I take a look at literally anything the Haskell people do and realize that it probably wouldn't have helped.
"""During his own Google interview, Jeff Dean was asked the implications if P=NP were true. He said "P = 0 or N = 1." Then, before the interviewer had even finished laughing, Jeff examined Google's public certificate and wrote the private key on the whiteboard."""
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.