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.
Yes, I quite realize, being something of a type-theory geek myself. What System F is not is a dependent type theory, with a proposition type and strong normalization, or even a propositional fragment in which proofs must normalize, or types dependent on values (which you need, in order to get proper propositional reasoning!).
A self-interpreting variant on Martin-Loef or Homotopy Type Theory would have been astounding! But that’s not what this is.
Decidability is not actually what we want here :-p. I could go into elaborate descriptions of what we want, but those would be theory-laden with my own ideas. Read my backlog on here to get an idea of the general direction I’m thinking in.
This result is not trivial, but it’s useful for talking about Turing-complete programming languages, not about logic.
ELI5?
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.
Of course, neither System F nor System U is actually a logic, so...
System F is a type theory which is a formal system which is an alternative to set theory, so...
Yes, I quite realize, being something of a type-theory geek myself. What System F is not is a dependent type theory, with a proposition type and strong normalization, or even a propositional fragment in which proofs must normalize, or types dependent on values (which you need, in order to get proper propositional reasoning!).
A self-interpreting variant on Martin-Loef or Homotopy Type Theory would have been astounding! But that’s not what this is.
Decidability has a price. So apparently you are dissatisfied by this result or consider it trivial. I think this buys a lot. Waht are you missing?
Decidability is not actually what we want here :-p. I could go into elaborate descriptions of what we want, but those would be theory-laden with my own ideas. Read my backlog on here to get an idea of the general direction I’m thinking in.
This result is not trivial, but it’s useful for talking about Turing-complete programming languages, not about logic.