I sit next to thousands of keys. Physical, shiny, golden keys, which unlock hundreds of rooms. My hands ache from the past hours of sorting these keys, meticulously hanging them on piercing hooks and carefully selecting a handful at a time to slip into opaque bags.
This was the most mind-numbing experience all summer, worse than staring at a blank wall; I could feel my brain cells shriveling up as they memorized 4-digit key codes and fruitlessly struggled to optimize a procedure that was inherently unscalable. (Reminds me a bit of my thesis, actually…) I was almost relieved when the office job I had accepted in return for summer housing turned into dealing with high schoolers (some snobbish and rude, and many forgetful but quite nice high schoolers). Other than the occasional interruption, I could spend my time trying to convince Coq that if I execute a function that produces a response… it produces a response1. Pretty straightforward, right? I do think a few high schoolers were rather frightened by the glazed, frustrated look I would give them when they asked me for a key and my brain was screaming at Coq. Even with these frustrations, discovering NPR podcasts on top of having time to do research, and the true care and generosity of Mario (the building manager) made the job quite enjoyable. The housing offer was incredible (even with dead, rotting rats in our garden-level room and the occasional flash flood that destroyed our rugs).
That aside, this job really made me acknowledge the power of the brute force algorithm; and why it really, really would have been better to optimize a lot earlier; and also why sometimes it just isn’t worth it after a certain point. I think I’m often drawn to brute force because it’s simply the first thing that anyone thinks of. Get all the balls into the bin over there? Just carry them over! Change the names on this Excel spreadsheet? Time to sit down and start typing (I think copy-paste still counts as brute force). Brute force just seems so innate2. Sometimes optimizations become so natural that we don’t even realize what was the original seed. Like cooking, or following instructions; it’s so natural to parallelize (e.g., chop two carrots at once, cook the rice while chopping), but is it really natural? I remember my frustration in CS124 as I found that my brain just had a predilection for conjuring up brute force algorithms.
And the problem with brute force is that, for the most part, it works. You just need enough power (or motivation), enough time, and usually very little skill. I brute forced Excel documents and key sorting, just as I brute forced the proof by typing the same tactics way too many times. The former was the fault of years of under-optimized processing, and the laziness of generations of student workers to care enough to spend days implementing better ways to sort keys and change names in exchange for cutting down on a few hours of work. (I probably could have written a program, but I think the computer was running Windows XP and I, too, was lazy). The latter was the fault of pure laziness: the fact that I knew it would work, and could I just spend another 20 seconds typing instead of writing an Ltac that would take potentially hours to perfect? 20 seconds, of course, multiplied by 100, or even 1000, is a lot. But I just couldn’t bring myself to optimize. There’s a fine balance between getting things done, getting things done quickly, getting things done “right”. I suppose the first is brute force; the second is optimization; and the third is ethical optimization. I guess I haven’t even satisfactorily done the first, but perhaps that’s because I haven’t mastered the others. We live through algorithms, so is such a mastery, more than anything else, worth discovering?