Hacker News Reader

Comment by jameshart | Hacker News Reader

Someone needs to tell the mathematicians they are allowed to use variable names longer than a single character now.

I can’t fathom anyone who has actually spent significant time performing mathematical manipulations with pencil and paper thinking that this is a good idea. Mathematicians have evolved notational conventions that work well for reading, writing, and calculation.

And I can't fathom why anyone would prefer to declare fundamental components of their proof using identifiers as terse as this:

   nominal_datatype fm =
       Mem tm tm    (infixr "IN" 150)
     | Eq tm tm     (infixr "EQ" 150)
     | Disj fm fm   (infixr "OR" 130)
     | Neg fm
     | Ex x::name f::fm binds x in f

These are not pencil-paper formula notation, they are declarations of named entities, and they don't need to. be so terse.

These are obvious abbreviations in the context. If you're working on a proof you might not want lots of 'theorem' and 'formula' to clutter up your screen.

The programming world converged on full word variables, but it also converged on {} instead of BEGIN END etc.

Alex

They fscked up when they decided to omit the dot when multiplying. So now it's impossible to differentiate between "varname" and "var*name".

> They fscked up when they decided to omit the dot when multiplying. So now it's impossible to differentiate between "varname" and "var*name".

Well, since we don't use multi-letter variable names, no such distinction is necessary! But if, for some reason, we did do so, then these two cases would be typeset in LaTeX as \(varname\) and \(var\,name\) (or, rather, \(\mathit{var}\) and \(\mathit{var}\,\mathit{name}\), since TeX correctly interprets \(var\) as semantically `var` anyway).

> Well, since we don't use multi-letter variable names, no such distinction is necessary!

You remember the story about the Fox and the Grapes, right?

If you need multiple letter variable names, your function may be too long, or you are using a language that does not let you express yourself.

Go programmers, too.

https://github.com/golang/go/wiki/CodeReviewComments#variabl...

They aren't using ASCII. They just invent new glyphs.

that elitism has to stop, people should design hyeroglyphs-free programming languages optimized for mathematical expressions and proofs should be written in it. The lack of IDE support in regular mathML or PDF math is astonishing.

Reply on news.ycombinator.com