So this assumes knowledge of an obscure theoretical programming language, and a dubious symbol replacement. Yeah...

It doesn't assume it, it's syntax, you can just use it without knowing where it comes from.

It's like english. You don't need knowledge in obscure proto-germanic linguistics to use articles in your sentences. But if you want to understand why we seem to randomly attach "a" before nouns— proto-germanic linguistics has the answer (probably, I just speak english I don't know where all its syntax originates).

Functional programming is common in university curriculum. Terrifying that it can still be considered obscure.

IIRC, Richard explain that in one of his videos about Roc. I have seen at least a handful of them.

I believe Haskell uses it as well.

my hot take: the language should accept \, but formatters should replace it with λ

Lean does symbols very well. You can just type \r and it will replace it with a right arrow as you type.

^\