[Link] Self-Representation in Girard’s System U

I had to google ELI5 :-)

First:

• Programs are sequences of commands, conditions and different forms of repetitions. The form of these programs follows a very strict language.
• Types are a kind of language describing the words and numbers used in programming languages (or in math).
• Interpreters are programs that look at the description of programs and do what the commands say.

OK, now what the result means is that Brown and Palsberg achieve to create a system of types that allows to formally describe the objects (words, numbers) used in interpreters that can interpret themselves.

Why is that astonishing? Interpreters have been around for a long time, or? Including those that interpret themselves (which is called bootstrapping). Yes, but most of these use only very simple types. The power of the types used in a programming languages limits the way one can reason about the programs in the language. For the simple lamguages the interpreted programs are just a bunch of words. It is not possible to state that the bunch of words is a valid program. The System F mentioned above is quite powerful mathematically speaking. Fω even more. But both were not able to describe a program which interprets itself as valid program. This was achieved by System U.

I like how you made this comment, and then emailed me the link to the article, asking whether it actually represents something for self-modifying systems.

Now, as to whether this actually represents an advance... let's go read the LtU thread. My guess is that the answer is, "this is an advancement for self-modifying reasoning systems iff we can take System U as a logic in which some subset of programs prove things in the Prop type, and those Prop-typed programs always terminate."

However, System U is not strongly normalizing and is inconsistent as a logic.

So, no.

This is no major result indeed. Neither necessary nor sufficient. But if you want safe self-optimizing AI you (and the AI) need to reason about the source. If you don't understand how the AI reasons about itself you can't control it. If you force the AI to reason in a way you can do too, e.g. by piggybacking on a sufficiently strong type system, then you at least have a chance to reason about it. There may be other ways to reason about self-modifying programs that don't rely on types but these are presumably either equivalent to such types - and thus the result is helpful in that area too - or more general - in which case proofs become likely more complicated (if feasible at all). So some equivalent to these types is needed for reasoning about safe self-modifying AI.