(Untitled)

[gwillen]

I know I never post, but this is far too beautiful not to link to, and you should read it.

http://worrydream.com/LadderOfAbstraction/

(I like it totally independent of the random dig at the practicality of type theory, near the end. But I did laugh.)

Comments

[_tove]

Cute!

[aleffert]

I had a meeting or two with him at Apple. Smart guy. You might also like http://worrydream.com/KillMath/

[_tove]

this is so good

[lindseykuper]

Yeah. Dan Friedman says that the reason he's been excited about logic programming, relational programming, and proof assistants for the last ten years is because of the possibilities for interactive development and discovery. He often speaks of the "accidental proofs" that just turn up when a curious person starts messing with miniKanren.

[oniugnip]

That's so huge. We need generalizations of this sort of tool.

Maybe Processing is a good step in that direction, or StarLogo...

[oniugnip]

Oh wow, or the rest of the software on his site!

*inspired!*

[lindseykuper]

Or the writing, or the pictures, or everything.

At Mozilla, there's someone who showed people this page as an argument for why they should come work for Mozilla.

[shaktool]

Scratch!