sisob: You could, of course, compare to the Python version. This is for Gtk+ 1, but I gather that the interface for 2 is even cleaner (I just couldn't easily find a tutorial with an example I can hack). This example is straight from the tutorial, except hacked to do what your version does.

Some concessions to the Advogato/HTML limitations: I usually prefer to indent functions, even those with one statement. However, I wasn't sure how to get it to look right, so "def hello" is not idiomatic :( [but still works!].

Note how Python didn't make me define a class or even a top-level function. Of course, I could, and the earlier versions of this hack actually this have this. But I really want to make the GUI answer to <code>print "Hello World"</code> (which is a valid Python program that...well...).

import gtk

window = gtk.GtkWindow(gtk.WINDOW_TOPLEVEL)
button = gtk.GtkButton("Hello World")
def hello(*_): print "Hello world"
button.connect("clicked", hello, None)
window.add(button)
window.connect("destroy", lambda *_: gtk.mainquit())
window.show_all()
gtk.mainloop()

shlomif: I easily found a version that has been posted in '99: Here. Enjoy!

They have excellent quotes from the Neo-Tech pages there.

(And no, it is not OK to cheat at poker. It is ok to "bluff" at poker -- bet higher than it would be strictly rational to bet according to the odds. Do you really think it is ok to pretend to be people's friend, get them to play late into the night when they are too tired to think coherently, and then take advantage of them? Read the book about how to win at poker, or at least skim it, before trivialize its existence.)

raph: That's not even the beginning of it (as long as you're not too attached to "reverse chronological"). Some use it to write random rants about thoughts, others use it for purposes as varied as recommending commercial products to ranting about free software, while, and this has been a recent discovery for me, still others use it to create interactive fan-fiction. Of course, the non-personal blogs also vary: from free software, through geek community and ending in elitistic discussion sites, they cover all areas. However, you nailed one fact very accurately, and I thought it might bear repeating: Blogs are inherently webby: they are fun and useful because the web has, for all its limitations one advantage: however many links one puts, it does not disturb the stream of reading. Like in a certain horrible movie, they sit quietly, blued, asking us if we "want to find out more". They allow us to say what we mean by words like free without needing to launch the user into an argument he already knows. It even lets us inform the user how we feel about technical issues, such as threads without reiterating age-old arguments. Blogs fit the web naturally: the sponteneously create links. Google uses the web as an intelligent network of links. Thus, Blogs enhance the web in a way that Google is uniquely equipped to use to its fullest.

Like I said, I'm not saying anything that raph did not, but I hope I put an interesting enough twist on it :)

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.