The Nonlinear Library LW - Static Analysis As A Lifestyle by adamShimi
Jul 4, 2024
05:01
Welcome to The Nonlinear Library, where we use Text-to-Speech software to convert the best writing from the Rationalist and EA communities into audio. This is: Static Analysis As A Lifestyle, published by adamShimi on July 4, 2024 on LessWrong.
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...
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...