Older blog entries for jdybnis (starting at number 13)

In the eating

graydon speaks as if a test is a boring type of proof. I disagree that a test is a proof, and here is why. He formalizes the notion that testing some case, is equivalent to generating a proof for that case:

any test can be translated into a proof in a silly logic easily: the proof is simply the trace of your processor executing your program's code on your test's input, and the logic is one in which each machine transition that happened is an axiom. but that proof is boring

But remember that a test can fail to terminate. We are not converting the test to a proof, but the execution trace of the test. And that is an impossible task for tests that do not terminate.

Although it could seem like this is a silly technicality, it is big enough that you should not consider a test itself any kind of proof, unless it comes with a proof of termination. To me what distiguishes a proof from anything else, is that there is a totally routine way of checking if it is valid or not. A process that might fail to terminate, does not qualify as totally routine.

Testing Software Can Make it Easier to Prove Correctness

raph mentions Dijkstra's quote that testing can only show the presence of bugs, never their absence

Implied in this is that if you develop a formal proof that a program is correct, then the testing becomes superfluous. But in fact, some types of testing can reduce the burdon of developing the proof.

Instead of proving that a program is always correct, you prove a weaker condition. That is: if the program is correct in one case then it is correct in all cases. Then you write a test to establish that the one case you did not prove actually works.

One specialized version of this technique is, using a proof to establish the induction step of a proof by induction, but then writing a test in order to establish the base case.

sjanes71 and gary are right, directories suck.

Directories are a conflation of the distinct, and sometimes conficting, requirements of naming and classification.

For naming, we want identifiers that are globally unique and stable over time.

For classification, we want categories that are meaningful and can change over time.

The two sets of requirements are conflicting. In particular, we want categories to have globally unique identifiers, but we can not assume that they will have one globally-unique and unchanging meaning.

A lot would need to be done to replace the current system of directories in UNIX. It has a lot of inertia. Practically every program that interfaces with files expects them to be addressable with some variation of /foo/bar/baz. Plus it took a long time to create the stable, fast, and scalable implementations of the system that we have today.

xcyber: sort the tables then compare them.

ksandstr: what do you mean by an idempotent function?

Had a disappointing weekend, where I brought my new computer to an all night quake gathering, only to discover my computer would not run quake!

After hours of forcing other people to swap parts of my computer into their systems, I gave up hope of figuring out what was broken. I spent most of the night playing SSX on a playstation someone had thoughtfully brought with them.

The next day, during a second marathon troubleshooting session I discovered that my ASUS A7V motherboard + GeForce 2 + Win2k were not playing nice. The reason I didn't discover it earlier, was that everyone else had a GeForce 2 too. I should have installed Linux. :)

Anyway, I bought a new motherboard. Now everything is fine and dandy.

And I must say, Cygwin has a pretty slick install program put togeather.

Scheme

graydon:Yes, I think the right question is: "why isn't '() coerced to #f." More generally, why isn't the coerce-to-boolean form specialized for every type? The whole idea of everything being coerced to #t except for #f, in a way already violates the disjointness of types. If the system were totally pure, it would raise an error when anything other than a boolean constant is tested for truth. So, there is already a coerce-to-boolean form for each type; it just happens to be a constant function. I don't think it is any worse to define a more interesting coerceion function, different for each type.

Cognitive Illusions

I saw an interesting lecture yesterday on cognitive illusions in human/computer interaction; these are places where the mind incorrectly applys a hueristic to come up with a solution, instead of using logical thought.

One place this pops up is conditional probability. Write down the solution to the following problem before you check the answer.

Your friend has two rabbits. One of them is a girl. What is the probability the other one is a girl too?

For now, I've put the answer at the bottom of notes on my account page, because I can't figure out which of the allowed tags will make background black to do the hidden text trick.

Update: sarum is right, your friend wouldn't pick the rabbits randomly. So lets say, your friend has a rabbit that just had two children.

If you don't believe the answer, think about these other two problems, and how they are different.

There are two rabbits in a cage. The bigger one is a girl. What is the probability the other one is a girl too?

Update: and to clarify this one too, this question is not about rabbit physiology.

There are two rabbits in a hat. You pull one out, it is a girl. What is the probability the other one is a girl too?

Really tough to wrap your mind around, huh? If you still don't believe me, I'll make you a truth table.

Since Scheme seems to be a topic of discussion lately, maybe someone could answer a question for me.

Why is #f distinct from ()? For a language pushing minimalism, it seems unessesary.

Compare the following Scheme code to the same function in CL.

(define (breadth . trees)
  (if (null? trees) 
      () 
      (cons (map car trees) 
            (apply breadth 
                  (apply append (map cdr trees))))))

(defun breadth (&rest trees)
  (and trees
       (cons (mapcar 'car trees) 
             (apply 'breadth 
                    (apply 'append (mapcar 'cdr trees))))))

BTW, that person that was pestering me for a homework solution kept calling and emailing me, up to the day it was due, but I think someone else gave them help. Sheesh!

just venting

hehe