2 ms·

We did used to write programs that way, but as the programs (and machines) got larger and more complicated, we found it very hard to so we invented all kinds of

We did used to write programs that way, but as the programs (and machines) got larger and more complicated, we found it very hard to so we invented all kinds of languages and abstractions to help us think about programs. Why would an advanced intelligence be able to think about the large programs without similar tools? Moreover, why do you believe the AI will be able to write the program without special languages, but that it would still need a special language to verify the program? That’s the gap I’m not understanding.

pron 8d ago
It needs a special language for both. Machine code is a special language for programming, and since this is an exercise in imagining what an AI that could do anything would do, I don't see why it would need anything else. Machine code, however, follows the rules of a computer and not of those of a predicate logic, hence another language is needed for proofs. I've done my share of formal verification (see my old blog in my profile) and of programming in Assembly, and obviously the former is far harder than the latter. People have only managed to formally prove the correctness of programs (end-to-end) under ~10 KLOC. 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.
- ModernMech 8d ago
  But if it needs one language for programming, machine code, why is that the optimal and only one for every application? There’s not even one "machine code"; it’s per machine and each one has their own design constraints and quirks. Why should all semantic reasoning be duplicated separately at each machine code level rather than factoring common meaning above those targets and proving that the target-specific lowerings preserve it? 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.
  - pron 8d ago
    > But if it needs one language for programming, machine code, why is that the optimal and only one for every application? Why would any other specific language be? Machine code is the most general and, as I said, if the AI wants to use a compiler to, say, help generate code for other platforms, it can create one. > Also predicate logic can be expressed using machine code It can't. Predicate logic has certain deduction rules, and these rules are different from those of machine code (e.g. machine code doesn't have quantifiers or their introduction and elimination rules). Of course, the AI could invent an ad hoc logic language and write a prover for it, but in this thought exercise, I think the point is that people would want to verify the proven properties (and possibly the implementation of the proof checker). > 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? This isn't too relevant. If you need to build a skyscraper for tens of millions of dollars, you wouldn't spend much time thinking about how to lower the cost of the handle on the front entrance by $10. Even if every matrix multiplication is a little different, the proofs can be copied and changed slightly. The difference in cost of doing that or not is negligible compared to other aspects of the verification. Again, we write programs that are three orders of magnitude larger than the largest program we've ever managed to prove correct, and the difficulty does not scale linearly. So we're talking about an AI that's 10,000 or 100,000 times more capable than humans at writing software. Surely, matters as duplicating code and proofs are negligible for it. But even if it does matter, machine code isn't a problem because you don't have to duplicate manually. You can write the machine code that specialises the different applications and prove the correctness of that. This is like writing a small portion of a compiler. My general point is that proving arbitrary (practical) correctness properties of arbitrary (practical) programs is such a monumental achievement that anything more mundane, like a compiler, is trivial in comparison. It's like saying that someone can boil an ocean or move a mountain, but we must order them a taxi to get there.

pron 8d ago

It needs a special language for both. Machine code is a special language for programming, and since this is an exercise in imagining what an AI that could do anything would do, I don't see why it would need anything else. Machine code, however, follows the rules of a computer and not of those of a predicate logic, hence another language is needed for proofs. I've done my share of formal verification (see my old blog in my profile) and of programming in Assembly, and obviously the former is far harder than the latter. People have only managed to formally prove the correctness of programs (end-to-end) under ~10 KLOC. 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.

ModernMech 8d ago
But if it needs one language for programming, machine code, why is that the optimal and only one for every application? There’s not even one "machine code"; it’s per machine and each one has their own design constraints and quirks. Why should all semantic reasoning be duplicated separately at each machine code level rather than factoring common meaning above those targets and proving that the target-specific lowerings preserve it? 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.
- pron 8d ago
  > But if it needs one language for programming, machine code, why is that the optimal and only one for every application? Why would any other specific language be? Machine code is the most general and, as I said, if the AI wants to use a compiler to, say, help generate code for other platforms, it can create one. > Also predicate logic can be expressed using machine code It can't. Predicate logic has certain deduction rules, and these rules are different from those of machine code (e.g. machine code doesn't have quantifiers or their introduction and elimination rules). Of course, the AI could invent an ad hoc logic language and write a prover for it, but in this thought exercise, I think the point is that people would want to verify the proven properties (and possibly the implementation of the proof checker). > 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? This isn't too relevant. If you need to build a skyscraper for tens of millions of dollars, you wouldn't spend much time thinking about how to lower the cost of the handle on the front entrance by $10. Even if every matrix multiplication is a little different, the proofs can be copied and changed slightly. The difference in cost of doing that or not is negligible compared to other aspects of the verification. Again, we write programs that are three orders of magnitude larger than the largest program we've ever managed to prove correct, and the difficulty does not scale linearly. So we're talking about an AI that's 10,000 or 100,000 times more capable than humans at writing software. Surely, matters as duplicating code and proofs are negligible for it. But even if it does matter, machine code isn't a problem because you don't have to duplicate manually. You can write the machine code that specialises the different applications and prove the correctness of that. This is like writing a small portion of a compiler. My general point is that proving arbitrary (practical) correctness properties of arbitrary (practical) programs is such a monumental achievement that anything more mundane, like a compiler, is trivial in comparison. It's like saying that someone can boil an ocean or move a mountain, but we must order them a taxi to get there.