Proofs are a form of static analysis. Static analysis can find interesting bugs, but how a system behaves isn't purely a property of source code. It won't tell you whether the code will run acceptably in a given environment.

For example, if memory use isn't modelled, it won't tell you how big the input can be before the system runs out of memory. Similarly, if your database isn't modelled then you need to test with a real database. Web apps need to test with a real web browser sometimes, rather than a simplified model of one. Databases and web browsers are too complicated to build a full-fidelity mathematical model for.

When testing with real systems there's often the issue that the user's system is different from the one you use to test. You can test with recent versions of Chrome and Firefox, etc, which helps a lot, but what about extensions?

Nothing covers everything, but property tests and fuzzers actually run the code in some test environment. That's going to find different issues than proofs will.

▲

js8 2 hours ago | parent [-]

> Databases and web browsers are too complicated to build a full-fidelity mathematical model for.

I disagree - thanks to Curry-Howard isomorphism, the full-fidelity mathematical model of a database or web browser are their binaries themselves.

We could have compilers provide theorems (with proof) of correctness of the translation from source to machine code, and library functions could provide useful theorems about the resource use.

Then, if the AI can reason about the behavior of the source code, it can also build the required proof of correctness along with it.

	▲	chriswarbo an hour ago \| parent [-]
		> thanks to Curry-Howard isomorphism, the full-fidelity mathematical model of a database or web browser are their binaries themselves. Maybe I'm misunderstanding you, but Curry-Howard is a mapping between mathematical jargon and programming jargon, where e.g. "this is a proof of that proposition using foo logic" maps to "this program has that type in programming language foo". I don't see how that makes "binaries" a "full-fidelity mathematical model": compilation is (according to Curry-Howard) translating a proof from one system of logic to another. For a binary, the resulting system of logic is machine code, which is an absolutely terrible logic: it has essentially one type (the machine word), which makes every proposition trivial; according to Curry-Howard, your database binary is proof of the proposition corresponding to its type; since the type of every binary is just "some machine words", the proposition that your database binary is a "full-fledged mathematical model" of is essentially just "there exists a machine word". Not very useful; we could optimise it down to "0", which is also a proof that there exists a machine word. If we assume that you want to prove something non-trivial, then the first thing you would need to do is abstract away from the trivial logic of machine code semantics, by inferring some specific structures and patterns from that binary, then developing some useful semantics which captures those patterns and structures. Then you can start to develop non-trivial logic on those semantics, which will let you state worthwhile propositions. If we apply the Curry-Howard lens to that process, it corresponds to... decompilation into a higher-level language! tl;dr Curry-Howard tells us that binaries are literally the worst possible representation we could hope for.