[js8]

> 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.

[skybrian]

I'm not sure either of us really knows how Curry-Howard works, but my understanding is that it's a compile-time type system thing. In certain proof languages, a function that returns an int proves that an int exists (type is inhabited). And that's just not very interesting - you need more sophisticated types than we commonly use. Also, it only works for total functions, so it's not true in most ordinary programming languages.

So I'm skeptical that the code we write in ordinary programming languages proves anything interesting. Why do you think that?

[chriswarbo]

> 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.