Sounds like a bit much?

Dr. Thursday, that flower of a papist and programmer, writes

Wow.

I have just written the LARGEST piece of source code I have ever done in my entire life. The source code measures about a quarter of a gigabyte, and yes, that does include comments. In fact, one routine probably exceeds all the source code I have ever written, in my BS, my MS, my PhD, and over 30 years of industrial software development.

And even nicer, it is provably correct... the acedemics would drool at that.

So I did a silly little test: for twenty-seven seconds I typed out as quickly as I could an easy-to-think-of sequence, "one two three four..." and it came to 110 bytes, including some errors. At such a rate, without sleeping eating or other dull interruptions, it would take about two years, I had my machine tell me, to produce a quarter of a gigabyte. I actually don't think I could tolerate more than a couple hours of just typing on just one thing in any given day, so that forty years is a more reasonable estimate.

I can only imagine that something of the project involved an automation of the code-writing process; that would not only make the typing go swifter, it would also make the proof-checking simpler for, if you are careful, you can be sure that your helper-program only outputs correct code! Now, the Doctor assures us that his programs are doing something... something for him, though I'm quite ignorant as to what, except that one of them I'm pretty sure is writing the last of them.

Now, I don't really know why Dr. Thursday insists on having such a huge program to do I-don't-know-what, because there's a much shorter program that will do everything. Yes, everything. Well, given infinite space to work in, it will eventually do everything that can be done by an ordinary computer in finite time. It's called algorithmic search and takes about $n^2 \log(n)$ steps to run the first $n$ programs about $n$ steps each, unless they stop first. Now, admittedly, this is something of a blunt-force weapon, much like proving Wiles' Theorem That Settled Fermat's Last Puzzle by listing all the proofs possible. Now that we know it has a proof, we know you'll get to a proof eventually, but whether that happens before the next big crunch I don't know.

But, there it is.