Older blog entries for moshez (starting at number 34)

Writing Advogato Diaries

The next version of Twisted will come out of the box with an example that lets you write advogato diaries locally and send them to advogato. If you see this diary entry, this means that this example works :)

XML-RPC seems to be useful, for some things, after all.

Update!

The code is here

raph: thanks. The link you gave does give an explanation, but an incorrect one, I'm adraid :) Think about what you know: going from the design (even a fairly specific one) to a fully working program is, at the very least, a factor of 20 in length. Let's treble it for non-trivial proofs like Jordan, in which many techniques which are hard to formalize as stand-alone lemmas are assumed as trivial, and we have a factor of 60. So, basically, if we assume the "classical" Jordan proof is on the order of a 200k, then we estimate the formal proof to be 60*200k = 3MB. That's 3MB of no-comments, "assembly" level math. Now, sure, the checker will find bugs in that proof. How long do you think it would take to completely debug that insane amount of mathematical proof? Uniquifying names, proving each non-trivial set operation usage, and so on.

Yes, it is embarassing to have a referee find an error in your paper. I doubt it happens very often: mathematicians, before submitting papers, go over them with a comb looking for errors. Then they ask colleagues to look at them. Then they give talks about them. This is a much more efficient use of the time then translating it to assembly so the proof checker can verify it.

The author of the link you gave seems to argue that the proof checker will be able to fill in the missing details, because "computers are good at boring details". This is about equivalent to a statement that computers will be good at auto-debugging, because they're good at boring details. Computers are good at repetitive details, not mere boring ones. Significant AI increase has to happen before computers can fill in the missing details, even those which would be easy for first-year students.

Now, on the question of correctness proof, my skepticallity has no strict basis in experience, so I cannot argue as strongly. However, I do tend to think that in non-trivial programs, specifying the correctness correctly will be almost as non-trivial as writing the program.

raph: May I ask what the point of all these computer-verified proof systems? I mean, yes, we all proved in Logic 101 that it is theoretically possible, but seriously, what's the point?

Let me first clarify some things.

Mathematicians do have mistakes in their proofs, many times. However, I seriously doubt such a system will actually help solving that problem. I can speak with some authority, having a little experience in writing papers, that writing a complete proof of a non-trivial statement would quickly become onerous, and more bugs would be made in the translation.

I have learned, and taught, advanced math. Teaching math is about giving intuition through proofs. Proofs written up as formal list of statements give no intuition, nor an idea of how to solve similar problems, which is what teaching mathematics is all about.

It is a nice toy. It is even fun to enter a few simple proofs. But, having done some formal proofs, my experience is that the novelty wears off and it becomes a mechanical boring process (and I like this stuff, basically!).

So, I think I've discounted "helping mathematicians", "improving math teaching" and "having fun" as possible motivations. Either my logic is wrong (pun not intended) or I have not listed all possible motivations: which is it?

Thanks

kilmo: FYI, this characterisation of the Cantor group is awkward compared to the following characterisation. Take all infinite binary sequences. This is an additive group with the xor operation. Define the topology as the smallest one such that the set of all sequences which have 0 in the i'th place is both closed and open.

With this chracterisation you don't get an embedding the Cantor group on the line, but you do get an easy way to show all kinds of nice things.

Exercise: can you give this set another continuous group structure such that each element has order 0?

Hint: Can you give the set of all binary sequences of length n a group structure such that there are elements of order 2^n?

Thoughts About Legality

Yes, this has been done to death.

Background: I wrote the Twisted web client stuff (well, a lot of it, anyway). Playing around with some of the features, I came up with a simple script which downloads the Dilbert home page, parses it for the image name, and puts it in an IMG tag. Naturally, I wanted to put this example in the Twisted examples directory, because doing this in an async is a bit tricky, and it would be nice if newbies could see this stuff done.

glyph, the Twisted lead developer, vetoed it, for what seems to be a good reason: he claims it violates the DMCA. I certainly do not want to place my friends in legal jeopardy, so I refrained from adding it.

The script can now be gotten from my site. Please, download it and have fun with it. I hereby place it in the public domain, but it's more a toy than anything production-grade anyway.

It is annoying that this small hunk of cute Python code is illegal in the USA.

Thoughts About Usability

I am a very introspective person. When I feel a certain way, I would like to understand why I feel that way. I have wondered why I am so often irritated by people talking about usability in free software. An example of such an article (and a fairly good one, at that) is available from the GNOME Usability Project. I was trying to understand what the core of my irritation with the article. Then I stumbled on this gem:

Most of us probably want people to operate our programs, we desire "users"

And then it hit me. I don't.

I honestly don't care whether people use my programs. I write them to solve a problem. If the problem later comes up for someone else, I will point them at the solution I wrote (or helped write). Then, if it works for them, fine. If it doesn't, they're free to hack on it until it does solve their problem. They can, of course, not use it at all -- in which case I will usualy dismiss them as idiots, because I've already solved the problem, and move on with my life.

The only usability I care about is mine. I want to be able to use the programs I write. If nobody else can use it, that's perfectly fine -- as Franky says in Rocky Horror Picture Show: "I didn't make him.... for you!" [and the callback: "but she gets him anyway"]. This sums up my feelings. I don't make programs for others -- but they get them anyway, because I am careful to license them freely.

All this, of course, doesn't mean I don't care about bug reports. I try to keep my code clean and bug-free as I can. But, if there is a disagreement about what the program should do, at that point I will turn a deaf ear towards my users.

movement: I hoped it was obvious my lynx comment was somewhat tongue in cheek. Lynx is, of course, my browser of choice. Actually, I am not sure what "usability" problems lynx has, but hell, I am sure it has.

But I am quite certain it would be amusing to see MichaelCrawford submitting bugs to the lynx project along the same lines (I'm starting to think that his reports are being extremely unfair to his wife by portraying her in a classical sexist way as the "helpless female". One must wonder if she actually reads these bug reports, and if she does, what she thinks of her husband publically announces to the world that she is in tears.) Anyway, I use mozilla on my work machine, and I think I had one crash in a few months of using it, so as far as stability goes, I really can't complain -- my vague memories from my IE on Windows using time seem to indicate that this IE crashes more, so if we limit ourself to defining "qualities" by "number of crashes on preferred platform", Mozilla would get the upper hand. I also think mozilla is usable, but since I think vi, screen, zwm and differential topology are all perfectly usable and intuitive, you may freely disregard my opinion as someone whose mind is so Twisted to be actually sprained.

Gagh, I feel like I'm abusing my "Master" status (wtf is up with that?) by posting this, but whatever.

MichaelCrawford: I've seen you plugging (supposedly "subtly", but you're unsubtle even for a geek) your "skills" for a few years now, under the guise of writing "useful" and "informative" comments. Yet, for all that, I have yet to see one significant contribution from you to anything free software. I suppose I should make a technical exception to the "LinuxQuality" project, which is a contribution, perhaps, in the sense that like many other projects, it sits there gathering dust after you have finished your initial zest for contribution. The difference is that LinuxQuality rots on somewhere else than SourceForge. Yay.

So, let me recap, before I spout some more vitriol: you have achieved your Master status under somewhat false pretenses, you have made no worthwhile contributions to free software, you continuously whine about free software lacking quality (and your solution is to "lets all test the 2.4 linux kernel) and you confuse between usability flaws (where the software works fine and passes any conceivable test, but is hard to use) and crashes. You continuously whine about the supposedly high-quality of MacOS and BeOS, but you also try to tell them how to run their business (other people reading this: Michael has links to where he explains to MacOS and BeOS how to run their business on his site, if you care).

Now, your wife is in tears because IE has holes and Mozilla crashes. I am sure your wife is a perfectly intelligent person, and since she doesn't whine on public forums, I'll also assume she is nice and will conduct no personal assault on her person. However, perhaps in the interest of honesty, you might want to tell your wife to go ahead and use IE on Windows, if the only reason she's avoiding it is the security hole. Windows is inherently so unsafe, she shouldn't really count on avoiding using IE to save her from any malicious crackers. In fact, IE is relatively safe, as you'd need to own a malicious site (dangerous) or crack a benign site (and if you can do that, you can probably crack into your wife computer directly).

Alternatively, you can convert your wife wholly to Linux, with either Konqueror or Mozilla as her desktop. I'm sure (well, more like fervently hope, God knows I have no evidence) that you are competent enough to set it up for her and I'm certain you care about her enough to spend the two hours it takes to install Debian. Now, Debian is not imprevious to security problems. Hell, I get mail every two days about a security vulnerability. However, the Debian organization is careful and responsive to security threats, so your wife will probably be as protected as she can be with a computer which actually does something and connected to the internet.

As an added bonus, whenever your wife gets tired of bloatware like Moz or Konq, she can use what I use daily to browse the web -- lynx. Lynx, how do I love thee, let me count the ways. Since most web designers are totally incompetent idiots (well, this is the top 10% really, the rest are totally incompetent untrained monkeys), lynx just ignores their "design decisions" and displays their content. Since your wife designs web sites, I'm sure she would be interested to check that even without all the glitzy features, her site is still usable. So it's, basically, a win-win situation.

If your wife really really needs IE occasionally, to check the web site still loads OK, you can always just use VMWare to bring up Windows inside the Linux box.

As an alternative, you can put your money where your mouth is. Rewrite Mozilla on top of ZooLib. Surely, with ZooLib's wonderful abstractions, soon there'll be no more bugs in Mozilla, right?

But I am sorry for that last quip. Making fun of C++ is just not nice.

This is not really a diary entry, but rather a request for help: I couldn't find Fefe's address anywhere, and I want to contact him. So I decided a good way would to be to put in a diary entry to get into "recent entries". If anyone reading this has any connection to Fefe, please e-mail me at find-fefe@zadka.site.co.il. Thanks in advance.

Yesterday I was in Tel-Aviv meeting with clients. After the meeting, I met with Rami and Hezi for lunch. It was a lot of fun -- we made jokes, ate good food, and I started admiring Hezi for the way he talks to women. On the bus back I saw someone reading an article which started "XML is a new programming language". I guess they just s/Java/XML/ to last year's article. I restrained myself from telling him not to waste his time, and instead continued reading "Always Coming Home". I called up Chen to say hello and promise to give her the book when I'm done with it.