Comprehensive Proof Archive Network, Bittorrent for distribution
I wish math papers were something like literate Haskell for proof assistants. I'd like to be able to download a paper and execute the proof to check their reasoning. This would be useful only if there were a Comprehensive Proof Archive Network where you could download already proved theorems. I guess each research paper could be a library in that network.
I've been thinking about using bittorrent to distribute debian packages (or any other similarly centrally distributed set of files).
So far my idea is to get signed package listings from authoritative mirrors, and then use OpenSLP to find a nearby host with some of the packages, then use bittorrent to get them.
I have a new experiment today, I'm recording ideas on my iriver and then transcribing them to my blog later... and including the resulting mp3 files for download. If I get positive feedback about these mp3 files, I'll include more later. I if I hear nothing about them, I'll stop including them. Aren't you sorry I didn't start this yesterday with the Finnish entry?
UML is MP3 compression of parse trees. What other psychological compression could be used to describe the derivative of code?
Blogging as a responsibility.
Smart people will realize things that might seem obvious to them but are not obvious to other people. Therefore we each have the responsibility to write a blog. Upon further thought, everyone seems to realize somethings instantly that are just not obvious to other people. Some examples are the discovery of Huffman encoding in a college class, and the many theorems that were proven by students who arrived late in class and did not realize the problem on the board was an unsolved mystery. So everyone should keep a blog, they might find the one thing to advance our society dramatically.
Flip to the back of the back for motivation.
Sometimes when I get tired of looking at the dry detailed basis for something, I have to flip to the back of the book to see where I'm going. Whenever I get tired of looking at the beginning parts of Types and Programming Languages, I flip to the back and look at the dependent types section. That's where I want to go.
An especially crazy recent idea is that the stop part of bus stops is most of the problem. So I thought of a way to let the bus pick up and drop off passengers only by slowing down. The passenger section of the bus could be divided in half, and one half would be swapped out with a matching cabin at each bus stop. Then the people who want to get off would get into the cabin about to be dropped off, and the people getting would be waiting in the swap cabin.
My motivation for this idea is watching drunk guys taking five minutes to find their money and thus making me late.
I guess subways work the same way, though they use a lot more space to do it.