|
|
Friday, February 3rd, 2006
|
11:38a - reading about interactive media
To read later:
Alan Kay - the computer revolution hasn't happened yet seems to be a video about educational software.
Alan Kay - The Early History of SmallTalk
http://www.educause.edu/LibraryDetailPage/666?ID=COM9802
search for Mark Weiser's concept of "Calm Technology"
Note to self: Charles Simonyi has lots of money, might be interested in my ideas.
(comment on this) 
|
4:23p - the program-proof analogy
"claim" (How do you say "claim" in Coq?, i.e. an unproven starting point, usually used as a more readable compromise between forward- and backward-chaining) is analogous to a "macro let" (i.e. a 'let' that doesn't evaluate the init-values, but simply binds the declared symbols to code... what's the correct name for it?). In this analogy, a normal 'let' is a claim + proof (proof is evaluation).
Cut-elimination is analogous to macro-expanding this code: it's a way of getting a normal form for the proof/program (which may be interesting if you are interested in coding standards or in automatic programming). But it's a pretty stupid thing to do if you care about program-efficiency / proof-readability, since regular "let" stores the value of the computation (like memoizing), whereas "macro let" doesn't, and will compute the same value several times.
(1 comment |comment on this)
|
6:34p - emacs mode creation tutorial
An Emacs language mode creation tutorial
(comment on this)
|
|
|
|
![[info]](http://l-stat.livejournal.com/img/userinfo.gif){kind=small}
gustavolacerda's journal