Can a programming language based on Willard's Self-Verifying Theories [0] self-interpret in the limited sense established by Brown and Palsberg [1]?
Which is to say, what is the relation between a sub-Peano logical system that can prove itself consistent, and is complete, thus bypassing the 2nd Incompleteness Theorems, and self-referential decision problems posed in the programming language that corresponds to that logical system?
My suspicion is that such a language could provide very strong guarantees on the auditability of self-modifying code.
Which is to say, what is the relation between a sub-Peano logical system that can prove itself consistent, and is complete, thus bypassing the 2nd Incompleteness Theorems, and self-referential decision problems posed in the programming language that corresponds to that logical system?
My suspicion is that such a language could provide very strong guarantees on the auditability of self-modifying code.
[0] https://en.m.wikipedia.org/wiki/Self-verifying_theories
[1] https://www.semanticscholar.org/paper/Breaking-through-the-n...