moshez is currently certified at Master level.

Name: Moshe Zadka
Member since: 2000-07-09 07:17:14
Last Login: N/A

FOAF RDF Share This

Notes:

Those of you who received e-mail from me might have noticed my signature: There is no GOD but Python, and HTTP is its prophet. This is of course a parody of the Islamic "The is no GOD but Allah, and Muhamad is His prophet". It just so happens that whenever a network connectivity issue comes up, I always seem to end up proposing as a solution two Python programs talking via HTTP. Not only that, I've managed to implement quite a few of those proposals, and they worked remarkablly well.

Please note: I've moved my diary to my personal site. All further entries will be recorded there. My GPG fingerprint is: 4BD1 7705 EEC0 260A 7F21 4817 C7FC A636 46D0 1BD6 Contact me for public key!

Projects

Articles Posted by moshez

Recent blog entries by moshez

Syndication: RSS 2.0

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 :)

24 Dec 2002 (updated 24 Dec 2002 at 07:38 UTC) »

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.

33 older entries...

 

moshez certified others as follows:

  • moshez certified moshez as Journeyer
  • moshez certified effbot as Master
  • moshez certified gstein as Master
  • moshez certified faassen as Journeyer
  • moshez certified bernhard as Journeyer
  • moshez certified BrucePerens as Master
  • moshez certified ping as Master
  • moshez certified esr as Master
  • moshez certified amk as Journeyer
  • moshez certified mwh as Journeyer
  • moshez certified tigert as Master
  • moshez certified dalke as Journeyer
  • moshez certified MJ as Journeyer
  • moshez certified jwz as Master
  • moshez certified itamar as Journeyer
  • moshez certified rms as Master
  • moshez certified mjs as Master
  • moshez certified fejj as Journeyer
  • moshez certified NetHunter as Journeyer
  • moshez certified purcell as Journeyer
  • moshez certified alan as Master
  • moshez certified raph as Master
  • moshez certified deirdre as Journeyer
  • moshez certified Shenka as Apprentice
  • moshez certified kzin as Journeyer
  • moshez certified jhylton as Master
  • moshez certified mkrus as Apprentice
  • moshez certified shapr as Journeyer
  • moshez certified krftkndl as Apprentice
  • moshez certified Ward as Journeyer
  • moshez certified nowonder as Journeyer
  • moshez certified mbp as Journeyer
  • moshez certified gward as Journeyer
  • moshez certified nas as Journeyer
  • moshez certified joey as Master
  • moshez certified fdrake as Journeyer
  • moshez certified wichert as Master
  • moshez certified niemeyer as Journeyer
  • moshez certified nyh as Journeyer
  • moshez certified glyph as Journeyer
  • moshez certified carmstro as Journeyer
  • moshez certified z3p as Journeyer
  • moshez certified Jordi as Journeyer
  • moshez certified bdale as Master
  • moshez certified vorlon as Journeyer
  • moshez certified cjwatson as Master
  • moshez certified jml as Apprentice
  • moshez certified thom as Journeyer
  • moshez certified kwoo as Apprentice
  • moshez certified mulix as Master

Others have certified moshez as follows:

  • moshez certified moshez as Journeyer
  • itamar certified moshez as Master
  • mwh certified moshez as Journeyer
  • bernhard certified moshez as Journeyer
  • cbbrowne certified moshez as Journeyer
  • jae certified moshez as Journeyer
  • shapr certified moshez as Master
  • kzin certified moshez as Journeyer
  • Shenka certified moshez as Journeyer
  • faassen certified moshez as Journeyer
  • gby certified moshez as Journeyer
  • NetHunter certified moshez as Journeyer
  • nixnut certified moshez as Master
  • Dom2 certified moshez as Journeyer
  • nowonder certified moshez as Master
  • gward certified moshez as Journeyer
  • nas certified moshez as Journeyer
  • Tomer certified moshez as Journeyer
  • manu certified moshez as Journeyer
  • jrf certified moshez as Journeyer
  • fdrake certified moshez as Journeyer
  • shalabh certified moshez as Journeyer
  • niemeyer certified moshez as Journeyer
  • nyh certified moshez as Master
  • glyph certified moshez as Journeyer
  • splork certified moshez as Journeyer
  • demoncrat certified moshez as Journeyer
  • washort certified moshez as Journeyer
  • grant certified moshez as Journeyer
  • mulix certified moshez as Master
  • shlomif certified moshez as Master
  • lior certified moshez as Journeyer
  • ghaering certified moshez as Journeyer
  • mihtjel certified moshez as Journeyer
  • mglazer certified moshez as Master
  • lalo certified moshez as Journeyer
  • jdub certified moshez as Master
  • Jordi certified moshez as Journeyer
  • mattam certified moshez as Journeyer
  • z3p certified moshez as Journeyer
  • sdodji certified moshez as Journeyer
  • tfheen certified moshez as Journeyer
  • gene99 certified moshez as Apprentice
  • Netsnipe certified moshez as Journeyer
  • ariya certified moshez as Master
  • pphaneuf certified moshez as Journeyer
  • kilmo certified moshez as Master
  • walters certified moshez as Journeyer
  • ladypine certified moshez as Master
  • gt3 certified moshez as Master
  • Senra certified moshez as Master
  • Barbwired certified moshez as Journeyer
  • oubiwann certified moshez as Master
  • mhamilton certified moshez as Master

[ Certification disabled because you're not logged in. ]

New Advogato Features

New HTML Parser: The long-awaited libxml2 based HTML parser code is live. It needs further work but already handles most markup better than the original parser.

Keep up with the latest Advogato features by reading the Advogato status blog.

If you're a C programmer with some spare time, take a look at the mod_virgule project page and help us with one of the tasks on the ToDo list!

X
Share this page