[Question] What Programming Language Characteristics Would Allow Provably Safe AI?

It seems clear that many high-level pro­gram­ming lan­guages are can­di­dates for use in the first AGI. They have enough power to write that code. It seems clear, how­ever, that the power that those lan­guages have is in­com­pat­i­ble with for­mal safety. SPARK or OCaml are made so that it is easy to prove cor­rect­ness, which seems use­ful, but that’s not enough.

For ex­am­ple, we might need mem­ory safety to provide a for­mal guaran­tee that the pro­gram can­not di­rectly mod­ify the part of mem­ory con­tain­ing the re­ward func­tion, or the calcu­la­tion of the re­ward. On the other hand, it seems that Tur­ing in­com­plete­ness, which al­lows guaran­tee­ing that a pro­gram ter­mi­nates, would not be nec­es­sary.

So—what other (ex­tant or yet-to-be defined) types of lan­guage safety will be needed from a lan­guage to pre­vent a hy­po­thet­i­cally prov­ably safe AI from be­ing un­safe in prac­tice?