noblethrasher

Perhaps this one from Graham Hutton?

“A parser for things

Is a function from strings

To lists of pairs

Of things and strings”

Also worth noting that language that runs this very website was implemented in Racket.

Java's (Oracle's) strategy is to spend most the innovation on the runtime, and in that regard, it's probably the most advanced platform. The net effect is that you can write some pretty naïve and boring OO-style code that will almost always perform superbly. This is a good thing, and something that I envy as a C# programmer.

His PhD is in Computer Science.

Interestingly enough, the aforementioned quote was just an epigraph for a section whose penultimate point is that “mathematics is nature’s way of showing how sloppy your writing is”, followed by the ultimate point that “formal mathematics is nature’s way of showing you how sloppy your mathematics is”.

TLA+ really is quite nice. I write most of my TLA+ specifications longhand and only bother with the toolbox when I think that refinement might be useful. Even then, it's mostly for SANY rather than TLC.

After noodling with with the spec for half an hour or so, I’ll usually have enough insight/confidence to start coding/debugging.

I was just making reference to the fact that the guy that started HN originally planned to get rich by putting art galleries online.

Which, if true, would be hugely ironic.

Also, Thierry Coquand, who is behind CoC, and is also one of the developers of the software that became Coq.