The Fortress programming language was a research project at Sun that incorporated mathematical notation.
See page 24 of http://www.oracle.com/technetwork/systems/ts-5206-159453.pdf
They also had an ASCII-only representation for everything, so you could use a regular text editor if you wanted, kind of like Markdown.
Looking forward languages that will start making good use of Unicode! I am actually surprised Greek letters haven’t made it already. Lots of computer scientists are mathematicians that are used to math papers looking like an Ancient Greek tablet.