The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

Something that nerd-sniped me today: Suppose you are building a computer from the ground up, starting with building the hardware. You cannot use any other computers to build or verify anything; this is the only computer in the world, and you have only what you've built at each step. You have no languages, no operating systems, no compilers, no verification tools. All you can do is bootstrap.

Suppose you'd like to verify every single part of the hardware and software stack to the degree possible. It's OK (inevitable I guess) to start with unverified hardware, though, and replace it later with hardware you verify (has anyone done that? It sounds cool). You have two additional goals:

1) verify as much as possible at each each, and

2) minimize the TCB as much as possible at each step.

How would you go about this? What are the biggest conceptual barriers to this, if any? What is the smallest you can get the TCB at any step of the process, and in the end?

This is a purely academic and open-ended question, with zero practical motivation. It just sounds fun to think about and try, and like thinking about it might reveal interesting subproblems that actually have practical motivation.

Talia