Hi Bryce! I like this point a lot. I think however that there are several semantic features which are possible in my formulation, but not in yours. For example, it would be nice to have some safety features, such as certain kinds of memory safety, laid out, and then require that these features are preserved by any change to the language (so the agent must supply a proof thereof). I can imagine a number of safety criteria which I might want preserved in this fashion. Another, in a cryptographic context, might be “constant time” (more precisely: runtime is independent of secret inputs).
Hi Bryce! I like this point a lot. I think however that there are several semantic features which are possible in my formulation, but not in yours. For example, it would be nice to have some safety features, such as certain kinds of memory safety, laid out, and then require that these features are preserved by any change to the language (so the agent must supply a proof thereof). I can imagine a number of safety criteria which I might want preserved in this fashion. Another, in a cryptographic context, might be “constant time” (more precisely: runtime is independent of secret inputs).