leino.science
© 2020-2025, K.R.M. Leino
Any technical writer who uses formulas or variables ought to consider the issues brought up in this short article:
Many operators in programming languages have standard representations, like + and <. In
contrast, logical implication (⟹, “implies”) is an operator that different
programming/specification languages represent in different ways, particularly when the language
uses ASCII characters. I wish to make a recommendation to such language designers: choose ==>
over =>. Here’s why:
If you think of the boolean type as an enumeration consisting of the values false and true,
then many languages would let you compare these values with the ordering ≤ (“less than or
equal”). In ASCII, you would then write false <= true. Similarly, if you think of the booleans
as forming a lattice, then the common choice is to make false the bottom element and true
the top element. Writing the lattice ordering as ≤, you would again write false <= true in
ASCII. The ordering in the lattice is in fact the implication ordering, so ≤ is the same as
⟹. In typeset mathematics, one is used to this, so you may see both “false
≤ true” and “false ⟹ true”. But in ASCII, the situation becomes
confusing if you write ⟹ as =>, because then both false <= true and
false => true would hold. So don’t choose => as your implication symbol; choose something
else, like ==>.
Also, if you have implication, chances are you would also want reverse implication,
⟸ (“follows from”, or as Jan van de Snepscheut jokingly would say,
“explies”). If you had chosen => for implies, the natural choice for explies would then be
<=. But this would be disastrous, because then you’d have both false <= true (for “false
≤ true”) and true <= false (for “true ⟸ false”)! So, don’t choose =>
as your implication symbol; instead, consider ==> for implies and <== for explies.
Finally, although binding powers of operators are not chosen consistently across languages, I
like giving conjunction (logical “and”) and disjunction (logical “or”) higher binding power than
implication. To make the visual appearance of expressions suggestive of the binding powers, you
want to make lower-precedence operators occupy more horizontal space. A simple way to achieve
that is to make lower-precedence operators longer. Using 3 characters for implication instead of
2 achieves this effect: your eyes would naturally read A && B ==> C && D as (A && B) ==> (C
&& D), not as A && (B ==> C) && D. So, don’t choose => as your implication operator, choose
==>.