Muli Ben-Yehuda's journal

Swimming this morning, 1km (2×500). Got a cramp in my leg around 700m, but survived.

Day 10 was rather uneventful. Didn’t work out (gasp!) but did go out for a nice long walk in the evening with Orna.

Day 11 is today. As has become my custom lately, the first thing I did in the morning we get weighted. I’m already 1.1kgs down for this week, which is pretty damn nice, especially as I don’t feel particularly hungry. I think the intense exercise is paying off in increased metabolism, and that’s just swell.

Got to the gym in the morning, did a nice cross training session, which left me feeling great. That’s a pretty good sign that I need to increase the dossage, and I’ll be adding short runs after the cross training and before the weights starting from next Sunday.

All in all, I’m feeling good, and starting to feel some slack at the waste line of my pants. Yay!

“The Lisp Machine is a personal computer. Personal computing means that
the processor and main memory are not time-division multiplexed,
instead each person gets his own. The personal computation system
consists of a pool of processors, each with its own main memory, and
its own disk for snapping. When a user logs in, he is assigned a
processor, and he has exclusive use of it for the duration of the
session.”

“Each logged in user of the Lisp Machine system has a processor, a
memory, a keyboard, a display, and a means of getting to the shared
resources. Terminals, of course, are placed in offices and various
rooms; ideally there would be one in every office. The processors,
however, are all kept off in a machine room. Since they may need
special environmental conditions, and often make noise and take up
space, they are not welcome office companions. The number of
processors is unrelated to the number of terminals, and may be smaller
depending on economic circumstance.”

“The memory is typically 64K of core or semiconductor memory, and is
expandable to about 1 million words. The full virtual address space is
stored an a 16 million word disk and paged into core (or
semiconductor) memory as required. A given virtual address is always
located at the same place an the disk. The access time of the core
memory is about 1 microsecond, and of the disk about 25
milliseconds. Additionally, there is an internal 1K buffer used for
holding the top of the stack (the PDL buffer) with a 200ns access time
(see [CONS] for more detail).”

“The complete LISP machine, including processor, memory, disk,
terminal, and connection to the shared file system, is packaged in a
single 19″ logic cabinet, except for the disk which is
freestanding. The complete machine would be likely to cost about
$80,000 if commercially produced. Since this is a complete,
fully-capable system (for one user at a time) it can substantially
lower the cost of entry by new organizations into serious Artificial
Intelligence work.”

Oh, just go read the thing already 😉

Been reading a bunch of interesting papers and notes lately.

• 
  Thoughts on Social Processes and Proofs of Theorems and Programs, by
  De Millo et al., discussed on this blog previously.

• 
  The GNU 64-bit PL8 compiler: Toward an open standard environment for
  firmware development, W. Gellerich et al. This is a very
  interesting paper, describing the PL.8 (“80% of PL/I”) which is used
  for zSeries firmware development, and developing a gcc front end for it. (via Lambda the Ultimate).

• Lisp
  Machine Progress Report, by the Lisp Machine Group. Some choice
  quotes from this venerable piece of history coming right up. (via Lambda the Ultimate).

• Complexity
  (Notes on Works in Progress), by Jonathan S. Shapiro. Could’ve
  been called “why C is not my favorite language” (via listpmeister.com).

• 
  Compiler Optimization-Space Exploration, by Spyridon
  Triantafyllis et al. Interesting, but not earth
  shattering. Compilers choose optimizations based on heuristics, and
  heuristics are sometimes wrong. Trying all optimizations is time
  consuming. Let’s find a way to minimize the search space by only
  considering interesting heuristics, trying them, and choosing the
  best.

Date:   Tue, 18 May 2004 21:00:07 +0100
From: Al Viro
User-Agent: Mutt/1.4.1i
To: Mark Gross 
Cc: Christoph Hellwig, Tim Bird, linux kernel
Subject: Re: ANNOUNCE: CE Linux Forum - Specification V1.0 draft

On Tue, May 18, 2004 at 12:32:48PM -0700, Mark Gross wrote:
> These are some of the types of problems engineers at REAL software shops have
> to solve to be able to ship REAL product for REAL money.  If you haven't HAD
> to produce code like this yourself at some point in your carrier then you've
> lived a sheltered life.
>
> Its disingenuous for you to get on your ivory tower to point and laugh.

        Well, you see, after spending years cleaning up the excrements
of self-styled "REAL engineers" it's either get on the tower to point and
laugh or get on the tower to point and shoot.

This is a very interesting paper, available here. Its
main thesis is that formal program verification is inherently flawed,
and can never work. The argument in favor of formal verification goes
something like this: computer programming is like
mathematics. Mathematicians use proofs to show correctness. Proofs
start from point A and by a series of correct steps reach point B. If
A is correct and the steps are correct, B must be correct. We can
apply the same process to programs and show that they are correct as
well.

De Millo’s argument is that mathematical theorems are not
considered correct because of the mere fact that they have been
“proved”. They are considered correct because mathematicians discussed
the proofs with their colleagues, reviewed them, rephrased them in
their own language and applied them elsewhere, and thus came to be
convinced that the proof is indeed correct. It’s the conviction that
counts, not the mere technicality of the proof. With formal
verification, such conviction can never happen, since the proof is far
too long and unwieldy to discuss informally, or even thing about and
comprehend. One either believes that the proof is correct, or one
doesn’t, on blind faith alone. And blind faith, claims De Millo, is
not sufficient for us to trust a program.

While reading the paper, I kept thinking of what seem to me an obvious
solution. Open Source! Rather than looking at a “proof” or a program,
let’s look at the program itself. The source of a program can be
discussed, analyzed, modified and reapplied, in the same way that a
good mathematical proof is handled. A program, just like a
mathematical proof, is better if it’s simple. The similarities are
striking.

Near the end of the paper, I saw that De Millo apparently shares the
opinion, although he never comes out and says so. Figure 1, “the
verifiers’ original analogy” is:

  Mathematics    Programing
      theorem....program
        proof....verification

And Figure 2, “Our analogy”, is:

  Mathematics    Programing
      theorem....specification
        proof....program
    imaginary 
       formal 
demonstration....verification 

Note that the program in De Millo’s analogy is its own “mathematical
proof”.

Points to ponder: ok, so formal verification is inherently flawed, and
open source might be the solution. What now?

Last evening Orna and me went to an Italian restaurant. The food was a lot more oily than I expected, but Orna says it’s good oil, and the scales this morning tell me that no harm was done.

Morning workout this morning was so-so. I ate a small sandwich 30 minutes before the workout (bad idea), and my stomach was rather upset at first. Did weights first, and didn’t manage to sustain the usual intensity level. Cross training was fine, though.

After I did the cross training, while I was walking around, waiting for my pulse to slow down before doing the abs workout, there was a song by Warp Brothers on the TV. And a terrific thing happened – I really wanted to dance. Two of the things I really miss about being fit are dancing and running. There’s a long hard road to go, but I’ll get there, slowly and surely.

I should buy a gizmo to measure body fat percentage. Scales are treacherous and unreliable. I wonder when I can find one in .il.

… that a rice cake is actually tasty. As a matter of fact, I think I’ll have two!

gah, I can’t find a way to order the Navy Seals
Training DVD set to Israel. Unless I come up with something clever
soon, I’ll have to wait for the OLS trip (only 65 days to go!) and get
it in the US.

[muli] lxrbot countdown ols
[lxrbot] T minus 65d 13h 41s, (Ottawa Linux Symposium 2004) at Wednesday, 
July 21 2004.

Morning workout went very well. The gym was too crowded, but I didn’t let it bother me. I did the usual 30 minutes of cross training (483 calories burned, a new record!) and then the weights. I went easy on myself in the leg workouts, as my legs are still sore from the weekend, but made up for it in the pull ups and shoulder exercises, where I think I finally reached my limit. Of course, limits are made to be broken 😉

I haven’t woken up early enough to eat breakfast, though… and there’s another 40 minutes until lunch. Must be careful not to eat too much!

Oh, I got weighed this morning, and I’m up 100 grams from yesterday, which is nothing. That makes it 4.6 kgs down so far, and 1.6 kgs down since I started PNS training. I think I deserve this Navy Seal Training 3 DVD set from the Discovery Channel…