Static Analysis As A Lifestyle

post by adamShimi · 2024-07-03T18:29:37.384Z · LW · GW · 11 comments

This is a link post for https://epistemologicalfascinations.substack.com/p/static-analysis-as-a-lifestyle

Contents

11 comments

I’ve been watching French Top Chef (the best Top Chef, fight me) with my wife again, and I’m always impressed by how often the mentoring chefs, all with multiple michelin stars and years of experience, can just guess that a dish will work or that it will be missing something.

By far, whenever a chef points to an error (not a risk, an error), it’s then immediately validated experimentally: either the candidate corrected it and the jury comments positively on that aspect of the dish, or they refused to and failed because of that aspect of the dish.

Obviously, this incredible skill comes from years of cooking experience. But at its core, this is one of the fundamental idea of epistemology that experts and masters rediscover again and again in their field: static analysis.

The core intuition of static analysis is that when you write a computer program, you can check some things without even running it, just by looking at it and analyzing it.

What most programmers know best are type systems, which capture what can be done with different values in the program, and forbid incompatible operations (like adding a number and a string of characters together, or more advanced things like using memory that might already be deallocated).

But static analysis is far larger than that: it include verifying programs with proof assistants, model checking where you simulate many different possible situations without even running tests, abstract interpretation where you approximate the program so you can check key properties on them…

At its core, static analysis focuses on what can be checked rationally, intellectually, logically, without needing to dirty your hands in the real world. Which is precisely what the mentoring chefs are doing!

They’re leveraging their experience and knowledge to simulate the dish, and figure out if it runs into some known problems: lack of a given texture, preponderance of a taste, lack of complexity (for the advanced gastronomy recipes that Top Chef candidates need to invent)…

Another key intuition from static analysis which translates well to the Top Chef example is that it’s much easier to check for specific failure modes than to verify correctness. It’s easier to check that I’m not adding a number and a string than it is to check that I’m adding the right two number, say the price of the wedding venue and the price of the DJ.

It’s this aspect of static analysis, looking for the mistakes that you know (from experience or scholarship, which is at its best the distilled experience of others), which is such a key epistemological technique.

I opened with the Top Chef example, but almost any field of knowledge, engineering, art, is full of similar cases:

• In Physics, there is notably dimensional analysis, which checks that two sides of an equation have the same unit, and order of magnitude estimates, which check that a computation is not ridiculously off.
• In Chemistry, there is the balancing of chemical equations, in terms of atoms and electrons.
• In Drug Testing, there are specific receptors that you know your compound should absolutely not bind with, or it will completely mess up the patient.
• In most traditional field of engineering, you have simulations and back of the envelope checks that let’s you avoid the most egregious failures.
• In Animation, the original Disney animators came up with the half-filled flour sack test to check that they hadn’t squashed and stretched their characters beyond recognition

• 

But there’s something even deeper about these checks: they are often incomplete.

In technical terms, a static analysis technique is complete if it accepts every correct program (and sound if it rejects all incorrect programs, but that’s not the main point here).

Of course, there are no truly complete techniques in practice. This is because restrictions are powerful: the more you constrain what you and others can do, the easier it is to reason about it, and check much more properties. So type systems often forbid programs that would actually run without runtime errors, but which are completely messed up to think about. That way, they can provide more guarantees.

And this is even truer in much fuzzier fields like art. Most of the rules in art are not actual perfect boundaries outside of which everything is wrong. They’re instead starting points, first approximations.

If you restrict yourself to perfect intervals, like traditional western music for hundreds of years, it’s safe to predict your piece of music will work decently well.

Progress then manifests itself by an epistemic exploration of this rule, a curious probing, looking for which parts can be skirted, bent, broken, while still reaching your end. This leads to things like Jazz, which breaks most of the harmonic and rhythmic code of western traditional music. And it’s great!

Which is why maybe the most exciting part of watching Top Chef are these moments of grace where the chefs and the jury doubt the intuition of the candidate, but the latter just go “Nah, I can get away with that.”, and realizes it so well that it explodes the previous rule.

That’s not to say that these rules are useless. Once again, the productive position is rarely in the false dichotomy between the absolute rule and the useless constraint, but in the perpetual interplay between making the world simpler so you can reason more about it before acting, and just trying things out to push your model of what can work.

11 comments

Comments sorted by top scores.