I think the programming language could be key to a self-improving AI being able to prove that the new implementation achieves the same goals as the old one, as well as us humans being able to prove that the AI is going to do what we expect.

To me it seems like memory safety is price of entry but I expect the eventual language will end up needing to be quite friendly to static analysis and theorem proving. That probably means very restricted side effects and mutation, as well as statically checkable memory and compute limits. Possibly also taking hardware unreliability into account, although I have no idea how to do that.

The language should be easy to write code in — if it’s too hard to write the code, you’re going to be out-competed by unfriendly AI projects — but also easy to write and prove fancy types/static assertions/contracts, because humans are going to be needing to prove a lot of stuff about code in this language and it seems like the proofs should also be in the code. My current vision would be some combination of Coq, Rust and Liquid Haskell.

I think the programming language could be key to a self-improving AI being able to prove that the new implementation achieves the same goals as the old one, as well as us humans being able to prove that the AI is going to do what we expect.

To me it seems like memory safety is price of entry but I expect the eventual language will end up needing to be quite friendly to static analysis and theorem proving. That probably means very restricted side effects and mutation, as well as statically checkable memory and compute limits. Possibly also taking hardware unreliability into account, although I have no idea how to do that.

The language should be easy to write code in — if it’s too hard to write the code, you’re going to be out-competed by unfriendly AI projects — but also easy to write and prove fancy types/static assertions/contracts, because humans are going to be needing to prove a lot of stuff about code in this language and it seems like the proofs should also be in the code. My current vision would be some combination of Coq, Rust and Liquid Haskell.