Return the largest number possible in 512 characters of C

Well, I know how I would solve this problem if I was sufficiently good at packing really complicated damn programs into 512 characters of C, or if I were allowed, say, 10 kilobytes of code. Start with a large number X, a larger number Y, and a powerful proof system. For all programs of size X, search through all proofs of length Y to see if they prove that X terminates. Multiply the runtimes of all the Xs together, or pick the largest one, it won't make any difference.

In this case it doesn't matter much whether you use second-order logic or first-order logic, because what you can prove syntactically in second-order logic is no different from what you can prove in a many-sorted first-order logic. But you do want to pick a powerful proof system like ZFC that can prove the consistency of whole ordinal hierarchies of weaker systems, rather than something weak like Peano Arithmetic; that will make a rather large difference, because it means you'll be able to prove the termination of large recursive structures of programs that do their own searches through all possible proofs etc.

If anyone can come up with a method of producing substantially larger numbers than this using bounded finite runtimes and programs guaranteed to terminate, I'd be quite interesting in hearing it.

This is really deja vu all over again. Over 45 years ago I read a "largest number that can be computed with expressions on a postcard" competition in a publication of some college (details escape me as to which college). This was held over a number of issues, and much of this discussion echoes (as far as I remember) that competition. Then, as now, the difficult part was comparing two values computed in completely different ways.

What a weird problem. You're writing in C for a turing machine. Your program has to terminate but you can't use any real-world boundary like CPU time or memory, despite the fact that the most efficient ways of doing this sort of thing in C is to hack binary memory and cast a variable.

It seems like the people writing these programs had a much better idea of the problem definition than the description on the linked page.

This article is probably from 2002. http://groups.google.com/group/comp.lang.c/msg/3037543775aa8... I think that the title should have (2002) to make it clear.

for (;;) printf("9");