[sebstefan]

It reminds me of Lambda calculus

You can express `a + b` or `a * b` in their regular algebraic notation or you can express them as a lambda expressions

ADD = λab.(a S)n

MUL = λxyz.x(yz)

Manipulating these expressions instead of algebra, you can suddenly compute things such as "+ * +" (Plus times plus). That will yield you another expression for sure, but we don't even know what that means.

So maybe an analogy would be, it's like you developed a field where, from that mess, you could derive important insights and even turn them back into proofs

And there's debate on whether all invariants truly are maintained throughout the entire process

[bmn__]

> Plus times plus […] but we don't even know what that means

Yes, we do. https://youtu.be/RcVA8Nj6HEo?t=1017

[sebstefan]

The video doesn't say what you think it says