Lawrence Lessig has an essay in favor of limiting copyright terms. I agree of course, as I'm sure most Advogatans do. What struck me is his use of the phrase "lawyer-free zone" to describe the public domain, with the clear implication that this is a good thing.
I think that he's identified a clear cultural distinction between lawyers and non-lawyers. Lawyers, having been steeped in the legal approach to resolving disputes, assume that it's the best approach, and can barely consider any others. The rest of us recognize the legal approach as being hideously expensive, unreliable, often quite unfair, and with significant potential to limit innovation and flexibility.
These problems with the "lawyer zone", as opposed to the "lawyer-free zone", are the reason why the current trend to increase the reach of copyrights, patents, and trademarks is a bad thing. The problem is, of course, that most lawmakers come from the lawyer culture.
I'm impressed with Prof. Lessig for both being a damn good lawyer (his command of the legal issues as shown in his oral argument in Eldred vs. Ashcroft is downright impressive) and for being able to see and express so clearly the advantages of sometimes not doing things the lawyer way.
Free software, of course, is a shining example of an almost entirely lawyer-free zone. I'm impressed with the mechanisms we have for resolving disputes. One key, I'm now convinced, is fork rights. At heart, the right to fork a project gives people an option in case the current maintainer isn't doing a good job, for whatever reason.
A particularly clear examples is the handling of the SourceForge codebase. As the OSDir interview with Tim Purdue makes clear, VA Software did a number of things in direct opposition to the interests of the free software community, not least of which is making promises to release the code without any intention of doing so. A more subtle, but no less important, issue is the deliberate rigging of the installation process to make it difficult.
In the lawyer zone, these types of things would generally get handled as some kind of contract litigation. There'd be a lot of "discovery" to try to find a smoking gun to prove that this bad behavior was intentional, and in the end neither side would really win anything (in stark contrast to the lawyers themselves).
Fortunately, in the free software world, we have a better way. We simply fork the code, fix the problems, and move on.
I have high hopes that the Creative Commons can bring the benefits of the lawyer-free zone to writing, music, art, and other creative domains that have been increasingly dominated by the culture and processes of lawyers. We'll see!
Google's new stuff
Google absolutely rocks, but I'm not anywhere nearly as impressed with their more recent offerings.
I took froogle for a spin, but wasn't all that impressed. For example, the search "pc2100 ddr 512mb" gives you prices from $109.99 to $289.95 on the first page, while pricewatch is $96-$99 for the first page of the category. Other queries gave similarly unimpressive results.
I've written about Google Answers fairly recently. Here's how I think they (or someone else) could make a much more compelling service.
Very simply, start with the existing service but provide means of crediting user accounts for answering questions, in addition to debiting them for asking. Each user can choose to be in the red (as now), in the black (in which case Google would PayPal the money), or at zero, which is probably how most people would want to use it.
You have some nontrivial trust issues, especially as you're paying money out, but I'm pretty confident they're tractable. Google already has ratings, a dispute process, and so on.
Paying money to get an answer is interesting. It's a way for people to demonstrate that they really care about the answer, but at the same time it feels a little odd. On the other hand, if I can get an answer in return for answering 1.25 other people's questions, that would be appealing.
In any case, I find I have relatively little use for such a service, because I'm already part of a fabulous network of knowledge seekers. This diary is a significant component of that network. For example, one test query I was considering is the Latin translation of our family motto, "happy, sticky, and green" (in the sense of a child who has just eaten a pistachio ice cream). Now that I've posted the query here, the chances are excellent somebody will send an answer. Thanks in advance!
Why machine verifiable proofs?
But my main interest is not so much existing proofs of mathematics. What I really want to do is develop correct programs. The theorems needed for programming tend to be much too tedious for mathematicians to deal with. But if the programmer has the patience to generate such a proof, at least a mechanical checker can give pretty good confidence that the theorem is true, and thus that the program is correct.