Hacker News Reader

The program is a constructive existence proof of the theorem structures embodied in the type system.

I'm aware. I suppose I think of the theorems as less interesting though usually.