I'd really like to have everything written in Rust, not C. Rust does a lot of verification, verification that is very hard to understand. I'd like to be able to specify a function with a bunch of invariants about the inputs and outputs and have a computer come up with some memory-safe code that satisfies all those invariants and is very optimized, and also have a list of alternative algorithms (maybe you discard this invariant and you can make it O(nLog(n)) instead of O(n^2), maybe you can make it linear in memory and constant in time or vice versa...)

Maybe you can't examine what the LLM is doing, but as things get more advanced we can generate code to do things, and also have it generate executable formal proofs that the code works as advertised.