Audio note: this article contains 154 uses of latex notation, so the narration may be difficult to follow. There's a link to the original text in the episode description.

tl;dr it seems that you can get basic tiling to work by proving that there will be safety proofs in the future, rather than trying to prove safety directly.

This is not a new idea, e.g. here is Giles saying it 13 years ago. But this seems to me like it's relevant to a general answer for tiling, and I'd appreciate engagement, literature references, and discussion.

I'll keep this post self-contained, but here are some links to relevant discussion from the past.

Setup

I like the simplicity of the problem presented by cousin_it, and I'll adapt it for this post. It starts like this:

A computer program X is asked one of two questions:

• Would you [...]

---

Outline:

(00:50) Setup

(01:48) Accepting provably-safe successors

(02:37) Failing to prove ourself safe

(03:22) Regaining self-trust with a tweak

(04:53) But does it blend

(05:48) Musing on what remains

The original text contained 4 footnotes which were omitted from this narration.

---

First published:

Source:

---

Narrated by TYPE III AUDIO.