Lambda the Ultimate

A pretty funny video by Gary Bernhardt on some surprising behaviour in Ruby and JavaScript. I think Wat as a term of art for this phenomenon is quite appropriate.

There's also a follow-up blog post by Adam Iley explaining some of the behaviours in JS seen in that video, if anyone wants to understand the underlying semantics behind these behaviours.

Since we're all PL enthusiasts here, I expect everyone here will have their own lessons to take from this 4 minute video. Myself, it seems a perfect example of the dangers of implicit conversions and overloading. Stuff like this makes we want to crawl back to OCaml where overloading is forbidden.

Interactive Tutorial of the Sequent Calculus by Edward Z. Yang.

This interactive tutorial will teach you how to use the sequent calculus, a simple set of rules with which you can use to show the truth of statements in first order logic. It is geared towards anyone with some background in writing software for computers, with knowledge of basic boolean logic. ...

Proving theorems is not for the mathematicians anymore: with theorem provers, it's now a job for the hacker. — Martin Rinard ...

A common complaint with a formal systems like the sequent calculus is the "I clicked around and managed to prove this, but I'm not really sure what happened!" This is what Martin means by the hacker mentality: it is now possible for people to prove things, even when they don't know what they're doing. The computer will ensure that, in the end, they will have gotten it right.

The tool behind this nice tutorial is Logitext.