If you know a language with function types, then you can think of it as

  f : R -> R

that is, f having a type signature as a function, and

  f(x) : R

having a type signature of a float (or: being a float). And so on.

I've been using this approach to type-check calculus equations. Unfortunately the article in the top comment [0] says that

> Note that f means something different on the two sides of the equation!

so the Leibniz notation might be more ad-hoc than I thought, and I can't just type-check them, actually have to reverse engineer the intent of the authors. I have to think about this. For example I remember someone giving me 3 exercises from Stewart calculus, and I gave 2 back that those equations don't even type-check, maybe there are some notation abuses I am not aware of.

[0] https://mitp-content-server.mit.edu/books/content/sectbyfn/b...