Donald Knuth On NPR

StratoFlyer writes "This morning, NPR is running an interview with Donald Knuth titled Donald Knuth, Founding Artist of Computer Science. The persistence of this man is extraordinary, if not heroic. RealPlayer and MediaPlayer feeds will be available at 10am EST, according to the NPR.org site." Indeed they are.

Explain

The persistence of this man is extraordinary, if not heroic

What is that supposed to me? Especially the bit about "heroic"?

Re:Explain

Someone who accomplishes something important at great risk to his own life is a hero, not someone who plods along for years at a job no matter how important his contributions.

So what you're saying is, someone who is willing to (potentially) give up their life is heroic, but someone who is prepared to dedicate their life to a goal is not? That someone who gambles their life, knowing that they may or may not be successful and return to a 'normal' life is more heroic than someone who instead knowingly commits to spending the rest of their life, year after year, trying to achieve something?

Re:Explain

perhaps Mr. Knuth is a sandwich made on a long bun.

Donald Knuth on NPR?

Is NPR some kind of drug? If so where can I get some? I wan't to be on NPR too.

Re:Donald Knuth on NPR?

Is NPR some kind of drug?

Judging by the strung-out feeling this news junkie gets during the accursed pledge drive week, I'd say yes it is.

Re:Donald Knuth on NPR?

Yes, NPR is a mild sedative. Do not drive or operate machinery while listening to NPR.

I'll tell you what's heroic

Posting Realplayer feeds on Slashdot's main page. If they're available for more than 5 minutes, then that's heroic.

Re:I'll tell you what's heroic

Being in Real Player format they were unavailable to most of us even before they got posted on /. so there is no harm done.

Re:I'll tell you what's heroic

A Microsoft product, and a comparable non-Microsoft product are referenced in the article. The non-Microsoft product gets slammed first. I can't think of a better demonstration of the crappy corporate practices of Real.

Re:I'll tell you what's heroic

If you have mplayer configured correctly, you can download it (no streaming required) under Linux:

mplayer -ao pcm -aofile npr4532247.wav 'rtsp://real.npr.na-central.speedera.net:80/real.n pr.na-central/me/20050314_me_06.rm'

oggenc -b 64 npr4532247.wav -o npr4532247.ogg

rm npr4532247.wav

Ignore any spaces in the rtsp link (slashcode inserts them to prevent page widening). The link itself comes from the smil file you get when you try to listen to the show on the NPR site.

I have a script that uses a similar method to grab the latest episode of Car Talk every week.

Re:I'll tell you what's heroic

Woah.. that was easy.. I can see the Linux desktop revolution nearing!

Pretty good piece

Knuth came across as charming, and funny, and classically geeky, re-computing the size of a piece of paper necessary for making a five-pointed star with one cut and rattling off the equation behind it, or describing his mental process behind brushing his teeth, but also clearly grounded in continuing scholarly work.

The narrator also mentions he's "abandoned email." Interesting detail, especially as I contemplate the 995 messages in my inbox this morning (80% spam, 19% mailing lists), I am starting to wonder why I don't get around to it myself.

Re:I think he came off as having OCD

Well, let's hope you never apply for a job doing triage at a psychiatric hospital.

There's a world of difference between amusing yourself with puzzles and being obsessive. When you are obsessive, you can't stop yourself from thinking something even when it distresses or harms you.

Being enormously smarter and more creative than the average person is a form of weirdness, but not a form of sickness.

Re:I think he came off as having OCD

History is full of examples of geniuses that were barely balanced between the two,

Yeah, Isaac Newton for one. See Will Dunham's book "Journey through Genius" in which he describes a disgusting little experiment Sir Isaac performed with a pointed stick and his eyeball.

Just because someone is functional doesn't mean they're normal and not sick.

I'd say if a person is productive in society, and happy, you're going to have a hard time convincing me that he's sick. Even Sir Isaac. This sense that somebody who is a genius is necessarily a bit sick is an attractive myth -- it consoles the great body of us that aren't blessed with genius.

Re:I think he came off as having OCD

The fact of our society is that if you sent them to the funnny farm, you'd have very few people left who were good at math.

Re:I think he came off as having OCD

The other way of looking at this is that being good at mathematics is a mental illness. I'm having difficulty understanding why you and the grandparent are considering Knuth's perfectionalism a bad thing. Is he anti-social as a result? Does his perfectionism prevent him from leading a safe, furfilling, life?

I see no evidence that it's doing any such thing. He's a brilliant mathematician and computer scientist, and that's all. The world is full of different people. It's also full of arrogant, scared, jerks who do not like differences.

Re:Pretty good piece

The narrator also mentions he's "abandoned email." Interesting detail, especially as I contemplate the 995 messages in my inbox this morning (80% spam, 19% mailing lists), I am starting to wonder why I don't get around to it myself.

He sure has: Knuth versus Email [stanford.edu]

Re: Getting Rid of E-mail

If someone sends me a snail mail letter, the quality tends to be much higher than e-mail. Electronic media tends to make things so easy that folks don't put much forethought into their writings? Want proof? Look at my comment history :)

Re:Pretty good piece

You can still send him an email. His secretary prints it out on a laser printer, and Knuth stops by and picks it up and reads it. If it's worthy of a response, he writes on the paper with what looks to be a mechanical pencil and snail mails it back.

Looking at his response to my email I sent him in 1999, I'm suddenly stuck with a mystery. How did he get my address? I don't see it anywhere on the email I sent him!

Re:Pretty good piece

You want to know how Donald Knuth found a piece of information? Maybe it's time to re-read Volume 3 [amazon.com]?

I'm sure that he found it by walking the paths from Stanford to your address using Dijkstra's alogrithm to find the shortest route. And he did it without ever crossing the Koningsburg bridge!

TeX

Donald Knuth is legendary in the computer science world for writing a series of must-have reference books called The Art of Computer Programming. Part cookbook, part textbook, part encyclopedia, these books are also considered by many to be technical and personal works of art.

Of much more practical importance to most: he is also the creator of TeX (from which LaTeX etc emerged). When he was dissatisfied with the way magazines printed his articles, he did what every other geek would have done, i.e. invented his own typesetting language. Et voilla.

Re:TeX

Not only that, but he chose a great numbering scheme for TeX. From http://en.wikipedia.org/wiki/TeX :

TeX has an idiosyncratic version numbering system. Since version 3, updates have been indicated by adding an extra digit at the end of the decimal, so that the version number asymptotically approaches . The current version is 3.141592. This is a reflection of the fact that TeX is now very stable, and only minor updates are anticipated. Knuth has stated that the "absolutely final change (to be made after my death)" will be to change the version number to , at which point all remaining bugs will become features.

So it's both useful and cool.

Re:TeX

When he was dissatisfied with the way magazines printed his articles, he did what every other geek would have done, i.e. invented his own typesetting language.

You mean he didn't piss and moan about it on Slashdot?

Re:TeX

he is also the creator of TeX

My personal Knuth story: in 1979, when I was just starting graduate school at the University of Illinois, Knuth came on campus to give three lectures as that year's Gillies Lecture [uiuc.edu].

At the time, the second edition of Volume I had just come out, and everybody was eagerly awaiting volumes 4 through 7. The lectures were all packed, and the great man, inventor of LR parsing and author of the definitive tome on computer science, spoke on...

typesetting and fonts.

Don't get me wrong, the lectures were interesting, but it didn't seem all that fundamental to computer science, if you get my meaning. 25 years later, we're still waiting for volume 4 to be completed, but at least the new editions of 1-3 had nice fonts.

The following year, Douglas Hofstadter came to campus to speak. This was fairly soon after Godel, Escher, Bach [amazon.com] came out, so we were all excited to see what cool and interesting CS things he would lecture on. His lecture turned to be on...

typesetting and fonts.

I guess it was just the thing to do at that time; little did I suspect that much of the productivity of US offices in the 90's would be spent selecting fonts for documents. I guess great thinkers are just ahead of their time.

Favorite part

He used graph theory to lay out his kitchen. The most connected resource? The trash can. It goes in the middle.

Re:Favorite part

A dog would probably be more aesthetically pleasing and environmentally sound, and has the further advantage that it will gladly walk to wherever the food is being discarded.

A goat will address a wider range of garbage, but has head-butting-related disadvantages.

Re:Favorite part

A dog right in the middle of the kitchen table? I'm not so sure about that.

Re:Favorite part

This is a great idea. Sometimes I imagine my ideal house, and the kitchen table would have a garbage receptacle right in the middle.

In my house, the garbage receptacles are seated around the perimeter of the kitchen table.

Molasses race

The Art of Computer Programming, vol. 4
vs.
Paul Graham's Arc
Stay conscious, audience: great minds think at a 'medium' pace. :)

Re:Molasses race

No... Medium Pace is the hot-but-not-too-hot jar of salsa.

Direct link to file in a Linux-playable format...

anyone ?

The page seems to set a cookie about your prefered video codec and you can't get direct link to the file, and it can either be a ".wax" or a ?"smil" file I cannot play.

Anyone gentle enough to provide a good ol' torrent or something ? and in a Linux-playable format.

Thanks

Book Revision

Heard the interview on the way to work. I love that he gives something like $2.56 or something to everyone who finds a flaw in the book. He has cut checks for around 20K so far and that the first Book had 90% of it's pages altered in some way because of that. We have the same kind of thing where I work. Free 6pack to anyone finding a non-sensical phrase embedded in our documentation. Everyone actually peer reviews documentation now.

Re:Book Revision

And even though he may have cut checks for 20K, he's paid much less. Many people who have received checks from Knuth have them framed, and won't cash them in.

Re:Book Revision

I love that he gives something like $2.56 or something to everyone who finds a flaw in the book.

It's a little jest. He awards $100,000,000 (in binary) to anyone who finds an error. In decimal that's $2.56.

Dyslexic editor gets it all wrong

It's actually Donald Knuth on RPN. And he says it?s the greatest cause of brain damage in computing.

Open Source editing

Interesting note (IMHO) If you look at his website, he is currently writing volume IV of the art of programming. He has posted drafts of chapters up and actively elicits feedback from readers. He goes as far as offering money for bugs found. Another one he adds is in his citations he wants full names...he will pay readers $2.56 per full name discovered on his list of incomplete names. This is a guy who understands the value of community development even when referring to the work of someone head and shoulders above the community.

Re:Open Source editing

They also mention it in the TFA.

But I hate how you refer to this as 'open source'. Can you change Knuth's books any way you want and redistribute them? Nope. So really, it is nothing like open source or free software, except for inviting collaboration.

And collaboration did exist long before OSS. Academic peer-review has been around for a hundred years. And collaboration has always been popular in the academic world. It was uses within academic collaboration which turned ARPANET into the internet. It was the collaborative ideals of the academic world which inspired RMS to create free software.

So, IMHO, calling this 'open source editing' or talking about 'open source science' is really putting the cart in front of the horse.
(Not that academia hasn't been influenced by OSS/Free software, but since OSS/Free Software also originated there, that's what you call feedback, not a new and direct influence.)

What I found interesting.

"Do you believe that is a God?"
Knuth, "Yes I do."
Mr. Knuth goes on to talk about how it is good that there is no proof for God because makes him think about God. If there was a proof for God he would just solve it and to on.

This must make many people on Slashdot very happy. I have seen many posts claiming that only an idiot would believe in God. Think of how many people now have proof that they are smarter than Donald Knuth.

Re:What I found interesting.

Wouldn't that be Queen of San Francisco?

Re:What I found interesting.

Agnosticism, on the other hand, is saying "There is no evidence for God, but I choose to neither believe nor disbelieve." How crazy is that?

Not crazy at all, it is the foundation of science and critical thinking.

Do you also choose neither to believe nor disbelieve in invisible pink elephants? There's no evidence for them either, but if someone told you they existed, would you keep an open mind about that?

Yes.

An agnostic, however, sees the lack of evidence and yet continues to hedge his bets. Why?

It is not "hedging your bets." And there is no way of seeing a lack of evidence. That's the point -- get it? A scientific mind can only consider the evidence and form hypotheses, not the lack of evidence.

Here's a thought-experiment for you. It's 1940. The atom is the smallest element known to man. Does this mean there is nothing smaller?

Re:What I found interesting.

No, actually, it's not. Having an open mind is one thing, having a mind so open your brain falls out is quite another.

I have heard this quip before, but you are mis-using it when applying it to scientific and critical thinking. The original quote is making reference to people who will BELIEVE anything. Scientists must consider all possibilities until proven wrong.

This means invisible elephants MIGHT exist. However, as there is no proof that they do, and no theory for why they might, a scientist will not ponder the question long.

This also means wormholes might exist, and even though there is no evidence of them, scientists are open to the possibility because they'd fit in with other theories that are out there, and so they do consider these.

If someone told you there were invisible pink elephants in his back yard, you would keep an open mind about that and not think that maybe your buddy had flipped his lid? Even after going out and pointing out to your buddy that these elephants left no tracks, dung, or anything else behind to show their presence, or that you could walk over every inch of his back yard and not run into one, you would still choose not to disbelieve him if he insisted they existed and were there? Seriously? That's not science or critical thinking, that's just being foolish.

Would I disbelieve him? Of course. Would I go further and, without proof, tell him there is no way on Earth? For pink elephants -- probably so. For something much more mysterious, why bother?

I know you keep wanting to bring up these pink elephants, however the reality is that agnostics do not worry themselves over the question of God. There is neither proof or disproof, and so it is an interesting but pointless thought experiment.

For someone to see a lack of evidence and firmly come down against something is just as bad as firmly coming down in favor of it. This is why people often call Atheism a religion.

In addition, I would wager that many people that refer to themselves as atheists actually mean they are agnostic, but are perhaps not familiar with that terminology. Many of my so-called atheist friends would admit they are agnostic if you questioned them about what they really think.

Re:What I found interesting.

"For someone to see a lack of evidence and firmly come down against something is just as bad as firmly coming down in favor of it. This is why people often call Atheism a religion."

Hogwash. If someone tells you there are magic elephants in their back yard that can not be detected by any means, you have no evidence that they are right and no evidence that they are wrong. If choose to beleive that there are elephants, or choose to beleive that there are not, well, I say one of these positions is more reasonable.

An agnostic would say, it is impossible to determine for sure whether the undetectable elephants exist. This is true, so perhaps that makes me an agnostic.

An atheist would say, "I do not beleive there are elephants". Thus, I am an atheist. Perhaps Atheists and Agnostics are not entirely disjoint sets.

You seem to think an atheist has to say "There cannot possibly be elephants.", but this is not so. Atheist do not (all) say God is impossible. They say they do not beleive God exists.

I do not beleive God exists. I do not beleive undetectable elephants exist. I do not beleive either of those beleifs can reasonably be called a religion.

I submit that it is you who do not understand the terminology. You are not alone. Many people seem to like to redefine Atheism to mean only super-extra-strong-to-the-point-of-obvious-falacy Atheism. This is dumb, because I know of no one at all who subscribes to that beleif set, and so Atheist becomes a useless term. It seems much more useful to ditinguish between people who do not beleive God exists, people who do, and people who are undecided.

Re:What I found interesting.

In terms of the scientific method, the difference between atheists and agnostics is their view of the theory "God exists". Atheists consider this a testable theory, and the lack of convincing evidence supporting that theory (or any supernatural theory, for that matter) means to them that there is room to doubt that theory. Atheism does not imply a blind rejection of God, nor does it have anything to do with the rejection of organized religion. However, atheism is frequently associated with scientists, who frequently also reject organized religion, so atheism has gained that connotation by accident. Also, some very loud people who call themselves atheists blindly reject God without consideration - these are just zealots of a different nature.

Agnosticism is very similar to atheism with one key difference: agnostics believe that the theory "God exists" is not testable, and is thus disinteresting from the point of view of science.

Some view this as the "easy way out" of the deist question, but it's actually just another way of looking at the question from a scientific perspective. A theory must be testable in order for it to be verified or rejected through experiments. Theories which are not testable are nothing more than nice ideas or speculation from the perspective of science.

Most atheists and agnostics are not openly hostile to organized religion, but some are, and the rest of us get a bad name because of these loud few. Please do not associate atheism or agnosticism with anything more than differing opinions on how the scientific method should be applied to the question of God. Both atheism and agnosticism are closely related and in a different class from all other beliefs regarding God, in that they both reject faith as a way to find truth of God's existence or lack of existence.

Re:What I found interesting.

Douglas Adams on agnostics:

People will then often say "But surely it's better to remain an Agnostic just in case?" This, to me, suggests such a level of silliness and muddle that I usually edge out of the conversation rather than get sucked into it. (If it turns out that I've been wrong all along, and there is in fact a god, and if it further turned out that this kind of legalistic, cross-your-fingers-behind-your-back, Clintonian hair-splitting impressed him, then I think I would chose not to worship him anyway.)

Re:What I found interesting.

Donald Knuth is actually a Christian and has written a book [stanford.edu] where he analyses chapter 3 verse 16 of every book in the Protestant Christian bible. Each verse is illuminated with beautiful caligraphy.

He also gave some lectures about religion called Things a Computer Scientist Rarely Talks About [stanford.edu].

Re:What I found interesting.

I have seen many posts claiming that only an idiot would believe in God. Think of how many people now have proof that they are smarter than Donald Knuth.

I'm impressed that Knuth actively contemplates the existence of a god, and that he is willing to acknowledge his belief in public. That does not convince me that Christians (or Bhudists, or Muslims or Shintoists, ...) are smarter than athiests or agnostics.

For me, Knuth's belief in a god does not have the same authority as his ability to prove the efficiency or convergence rate of an algorithm. Mathematics and other branches of science are a rational and testable form of knowledge. Belief in a diety must ultimately come down to a personal choice -- a leap of faith -- beyond the realm of rational.

I have contemplated this leap and find a deeper mystery and deeper satisfaction and deeper challenge in not believing in the existence of god. That does not make me smarter than Knuth. It just means that we have reached different conclusions about a very personal matter.

The responses to this post are fascinating

It amazes me how many of the responses to this post managed to so thoroughly misunderstand it, and how defensive the reactions were.

Some posters responded by saying, essentially, "Just because he's a smart computer scientist doesn't mean I have to believe what he says about religion." This is obviously true, and a very interesting response because no one suggested that you should believe what he says about religion. What the OP was saying, for those who need it to be spelled out, is that people who try to tell others they shouldn't believe in God "because only stupid people believe in God", need to rethink their position. Not that they need to start believing themselves, but that they should admit that belief in God is not evidence of stupidity.

The OP wasn't ridiculing unbelievers, he was ridiculing the intolerance and arrogant condescension of some unbelievers.

The responses I found really funny, though, were the ones who jumped right in and essentially repeated the claim that people who believe in God are stupid, in a knee-jerk reaction triggered by the word "God", apparently completely oblivious to the fact that they had just been lampooned.

The absolute best of the bunch, though, has to be the one who claimed that the fact that Knuth is Christian places his computer science research in question! That has to be the epitome of closed-minded stupidity -- to base a rejection of well-founded research on grounds of a gently-stated opinion on a non-scientific matter... mind-boggling.

Re:Shhhh!

There all idiots who can't even spell!

The art of the elegant troll.

Re:What I found interesting.

A classic experience relating to my perception of fundamentalism was w/ a friend's child who was finally taken to see her grandfather's workshop (he was a classic old-school cabinetmaker w/ the only power tool in his shop a band saw 'cause he couldn't find apprentices to do that sort of tedious thing who was said to ``make things by hand'').

The daughter on seeing the shop and the walls lined w/ neatly arranged saws, chisels, draw knives, planes, spokeshaves, clamps &c. shrieked, ``Mommy! You lied! Grandpa doesn't make things by hand! He uses tools!''

IME fundamental creationists exhibit a similar na{\"\i}vet\'e as to how God works.

William

Leftist crap

Look at those leftist NPR hacks, going and interviewing an actual computer scientist, rather than the business leaders, CEOs and MBAs who really make things happen. God, they just make me so mad, those commie Public Radio personalities with their "insightful" and "interesting" guests who think they're "oh, so smart" with their "science" and "knowledge" and "thoughtfulness" crap. Someone should shut them down! I want to hear a good old "Proud to be American" conservative commentator screaming at me and telling me how to think! God Bless Red America! Thank you and good night!

In a twist of fate, Microsoft announces Visual MIX

Most of us struggle with basic assembly language. But Knuth goes and invents his own VM (MIX) and programs all of his examples to it. You just have to admire that.

Not Slashdoted

Finally a good piece of news to share with the other guys that did not get slashdoted. This was definately a good article and a morning edition is always a good show to listen to.

Knuth was there first

Knuth was there first. When "Fundamental Algorithms" came out, there were almost no computer science books. There were vendor machine manuals, and books on programming languages. "A Fortran Primer", by Elliot Organick was about as good as it got. MIT students had a tech note series called HAKMEM, but few others saw those. There was a huge vacuum waiting to be filled. That's why "Fundamental Algorithms" got so much attention.

Re:Knuth was there first

Maybe he said it first, but the real kicker is that no one has been able to say it better since then.

MSH

I can get an OGG/MP3 if there's a place to put it

I'm not big on hosting it for the Slashdot crowd, but I can get an OGG/MP3 version of this if someone has somewhere to put it.

OT: It would be great...

...if /. would generate and post a bittorrent link for all the media files BEFORE the article is posted.

/. DDoS of content providers is so uncool.

(I realize that NPR was posting the file later today, but do you think you could have waited before posting the article? And then provide the bittorrent link?)

I'd like to hear this...

Well, since the article went up 40 minutes after the interview started, I'm wondering if anyone's captured the audio streams and put up a torrent?

I know, wishful thinking...

spoken word

Knuth's lectures are quite interesting. You can find some more of them here:

http://technetcast.ddj.com/tnc_catalog.html?item_i d=421 [ddj.com]

or by searching the eDonkey/eMule network for "donald knuth" or "god and computers"

Function over form.

10 years ago my profressor of CS (3rd year) made us us LaTeX to turn our papers in.

We all could have us MS Word but there was a point to be made.

They looked ugly and of poor quality. But higly efficient!! Aggh!!

10 years have passed and while driving in the Garden State Parkway I heard the interview of this uber pragmatic man and the creator of LaTeX.
Donald Knuth.
A ha!

I got to work, looked at the NPR site and then went to Professor Kunth homepage.

I knew what I was looking for and got it in all it's glory.
His homepage.
What an eyesore!
A not very complementary self-picture (he should use the one on the NPR site) and the BIG BOLD heading-1 letters for all the link under some colorless background.

It sure took my back to my first html site 1995.

Function over form, the trademark of scientific academia.
A brilliant man, nevertheless.

He should pay 5.12 to some student to do a extreme-make-over to his home-site. Some drop-down
menus..cool graphics..make it pretty!

256 Mistake

How ironic that in discussing Knuth's errors in his books, the reporter makes a mistake. 256 = 2^8, which is one followed by eight zeros, not seven, and hence looks like one hundred million, not ten million. I also find it amusing how he describes the "binary language" of computers. So different from that "decimal language" we humans use.

Artist?

Was anyone else with a comp science background mildly offended by being referred to as an artist?

A Knuth Story

There's no denying that Knuth is a great computer scientist, but his attitude toward those he works with can be appalling to say the least.

I was a grad student at Stanford in the early 90's. The practice then (and still probably now) was to shut down the CS department for a week or so during the December holidays, for the obvious reasons (vacations, spending time with the family, etc) An e-mail announcement was sent to that effect every year, so it surprised no one. However, Knuth spammed the entire department with a response to the announcement, questioning why we would close the department. I responded back with a reply, saying that our dedicated department staff deserved the time off.

Needless to say, I was the hero of the department for a few days.

Alternate world exercise

Now, let's just wonder for a moment how the world could look like if he had been less a scientist and artist but more a businessman and decided early on to charge for TeX... Or patent his works.

There are deaf admirers of Donald Knuth

and they would like to have a written transcript of the interview with him.

Why do you like Knuth?

I'm not trying to troll, but I really don't understand the fascination with Knuth and his work. Knuth clearly is an important computer scientist and some of his work has had a big impact, but he wouldn't be my choice for computer science hero.

I don't find "The Art" to be a particularly well written book--the verbal presentation is great, but I consider the selection unfocused and approach questionable. I have rarely come across anything actually useful in one of Knuth's papers. And have a look at his recent publications [stanford.edu]; is there really anything interesting in there? The one piece of software that I use of which I know that it is related to Knuth, I have a love-hate relationship with: TeX does something very useful and it does it technically well, but as a piece of modern software development or language design, I think it deserves a failing grade.

So, the question is: why are you so fascinated by Knuth? Which of his papers or results are you really fond of? And which of his results are you actually using? What examples of practical impact of Knuth's results can you actually give.

It has to be said...

....imagine a Beowulf cluster of Don Knuths.....

Not to be overly critical...

But I just wish he would do all his math in some kind of machine checked formal logic, it would make things easier to follow in his books. I know that people say that there are too many steps when you try do do a proof in formal logic, but we've come a long way, and most LCF based interactive provers, can do a lot of the grungy work for you, so you will still have the outline of the proof available. For example...

- val thm1 = PROVE [] ``~~A:bool = A``;
Meson search level: ....
> val thm1 = |- ~~A = A : thm

- val trm1 = ``x:bool``;
> val trm1 = ``x`` : term

- val trmTemplate = ``x /\ T = F``;
> val trmTemplate = ``x /\ T = F`` : term

- val thm = ASSUME ``~~A /\ T = F``;
> val thm = [.] |- ~~A /\ T = F : thm

- val result = SUBST [ trm1 |-> thm1 ] trmTemplate thm;
> val result = [.] |- A /\ T = F : thm

- show_assums := true;
> val it = () : unit

- result;
> val it = [~~A /\ T = F] |- A /\ T = F : thm

This might not be the best example (it's all I had at the moment) but as you can see in the first step, HOL proved ~~A = A, an obvious theorem that I couldn't find quickly in the library. HOL did this almost instantaneously, and routinely makes me look like a fool, proving stuff that will take me a half an hour in the blink of an eye. The user interfaces are a bit dated, but they have great potential for improvement.

Re:Abandoning Email is Stupid

He actually abandoned email in 1990 [stanford.edu]. The complaint was that email is for people who want to get on top of things, and he's the type of person who wants to get to the bottom of things.

In other words, he was getting legitimate email, and it was a distraction for that reason.

I'm pretty sure that if the problem was spam, Knuth is one of the few people who'd actually create a system that can, actually, filter spam and spam only.

he didn't abandon email because of spam

From his website: "Email is a wonderful thing for people whose role in life is to be on top of things. But not for me; my role is to be on the bottom of things. What I do takes long hours of studying and uninterruptible concentration. I try to learn certain areas of computer science exhaustively; then I try to digest that knowledge into a form that is accessible to people who don't have time for such study."

Re:Abandoning Email is Stupid

You know, perhaps spam's not the problem. Remember this is a very inventive man. If spam were the problem, he would either employ a solution or likely tackle it because it is a large hard problem.

Re:Abandoning Email is Stupid

Abandoning email may be stupid for you, but you are not Donald Knuth. Read his page on why he abandoned it [stanford.edu]. He dropped it in 1990, when SPAM was a lunchmeat.

On an unrelated note, I love this note on his page about The Art Of Computer Programming: [stanford.edu]

... And if you do report an error [in TAOCP] via email, please do not include attachments of any kind; your message should be readable on brand-X operating systems for all values of X.

Re:NPR

That's pretty bizarre - so they're promoting intolerance toward a particular news feed and censorship in the name of tolerance. The irony is killing me.

Re:Abandoning Email is Stupid

Post your email address when you say that, pilgrim.

Re:The Part Where He Doesn't Take Off His Bike Hel

But this bike helmet thing just doesn't make much sense (I could be wrong). I park my bike outside at a rack and then walk into the building. As I walk between the rack and the building, I can take my helmet off. It's nice to feel cool air on my head. When I walk out, I can put my helmet back on. What does he do, ride his bike directly into his office or something?

Re:NPR

I just automatically thought of the episode when I read your post. I agree that its sad that this counts as bold. I wish more media was politically charged. America is just so full of people who are either apathetic, know only the talking points of parties (meaning they don't want to think for themselves), or extremists. Nobody talks about politics or others up opinions. Our mainstream entertainment industry barely touches political topics and I find that a shame. I wish more entertainment would attempt to provoke discussion. Provoking discussion allows people to make up their own minds easier and not rely solely on one party's talking points because rarely is anybody perfectly represented by one party. The media loved discussing the red & blue distinctions during this past election but I think thats misleading. I think most people are in the middle but the problem is there isn't a mainstream party that represents a moderate. A moderate party would get eaten alive by both sides in our political system because they aren't "EXTREME."

Why are kids watching tv while at school?

Jesus. That's the fucking problem, not *what station* they are allowed to watch.

Re:The Part Where He Doesn't Take Off His Bike Hel

He never said it would take too long to remove the helmet. He only said he would be coming back outside again soon anyway. What's the big deal? I've seen people wearing bike helmets inside buildings lots of times. I'm also seeing a lot of people here nitpicking little things about Knuth because they don't have any valid criticisms of him.

Good idea

Call someone at Microsoft, see if they can direct you to the right person.