In reply to @dginev
@dginev yes, I think that the relation between notation and quantities with types is something that most mathematicians don't really think about, but becomes a big problem when computers get involved
In reply to @christianp
@dginev in this instance, I'm specifically interested in the notation