The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Thanks for drawing attention to a worthy goal, which I think at least a few different research groups already have in mind, at least philosophically.

For such an effort, setting the goals properly can have a big effect on where it winds up.  I'm not sure it makes sense to ask to "minimize the TCB as much as possible at each step."  Rather, I'd expect that earlier stages are discarded as they are used to produce later stages, and the final stage can be used independently for self-validation.  So, shrinking the TCB in an earlier stage isn't necessarily a good deal, if it delays the completion of later stages.

There are plenty of high-impact proof-assistant developments that never could have been completed so soon if e.g. the original Coq team had decided to wait 20 additional years for the first release, to shrink the TCB as much as they could think up in brainstorming a project roadmap!

Also, I don't think this question has zero practical motivation.  I would hope that, 50 years from now, everyone takes for granted the existence of a repeatable process like you describe, leading to the systems they depend on.  And, even sooner, we should be able to run undergraduate courses that follow such processes toward more modest endpoints.

On 1/8/22 1:41 PM, Talia Ringer wrote:

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