Following this tutorial you can have any symbol at your fingertip when typing on a Linux or *BSD system.
Write readable LaTeX files, with
$A = πr²$ instead of
$A = \pi r^2$ in the source.
Agda, is a dependently typed language for programming and proof-verification. Here is how I write it, using the Acme editor.