Also predicate logic can be expressed using machine code, so why does the AI need a whole other notation to express predicate logic? It should just be able to use whatever machine code it used to write the program.
If the answer is that the verifier would benefit from extra semantic information in the logic language, then why doesn’t that same representational argument apply to programs? Programs also have semantic structures that aren’t naturally expressed by the ISA. E.g. types, effects, state machines, matrix operations, synchronization, ownership, capabilities, protocols, etc.
Moreover, why can’t this hypothetical AI just write correct code that doesn’t need to be proved through predicate logic?
> If for some reason an AI capable of writing and proving arbitrary programs thinks it will be aided by a compiler, surely it will be able to create its own ad-hoc one for the problem at hand.
I think this basically concedes my point: you’re saying the ai will create ad hoc programming languages to support its thinking, which I think is much closer to what will happen. I think it would choose to do this in nearly all cases. It’s one thing to be able to prove arbitrary programs, quite another to do so within resource constraints, like finishing the proof before the heat death of the universe.
Take for instance this expression:
A * B
Where A and B are matrices and * is matrix multiply.
The most efficient machine code for this will unroll all of the loops and multiplications and additions, pipeline and fuse them, and schedule them across parallel registers for SIMD instruction.
The machine code instructions to express just this one instance would be hundreds to thousands of bytes depending on the size of the matrix.
What’s easier: verifying the high-level matrix multiply to machine code lowering is correct (per machine) and therefore every application of it is correct; or that every single bespoke matrix multiply actually correctly implements matrix multiply for every machine?
At some level you’d spend more time proving every instance of bespoke unrolled matrix multiply machine code every time you generate it than just generating a permanent deterministic proven correct compiler and using that instead. I think a sufficiently smart AI would figure this out and absolutely take that shortcut, for the same reasons humans did.
The prover itself benefits from establishing higher level concepts as well, so there’s a real disconnect between the predicate logic and the machine code. The verifier would thrive on semantic information like: the matrix dimensions are fixed, the dimensions are compatible, the types are consistent, the values are immutable… all of that is intentionally missing by the time you lower to machine code (usually because it’s usefulness in proving the program have been exhausted). It would be better to hand these as statements of fact (determined by a type checker) to the verifier rather than asking the verifier to first prove them from byte code and then do the actual correctness proof.
Removing all that semantic information leaves the prover having to reinvent it on every proof. So I guess you could include that higher level semantic information in the machine code but now you’re back to designing a programming language.