The Coq mailing list

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

Thanks, yes, that makes sense. Someone else I was talking to brought up that minimizing the TCB at each step is its own interesting constraint, but not necessarily the best one if your goal is to minimize the TCB in the end, and to do it efficiently.

But if we do separate those two, it does kind of raise a question to me about what the final TCB really means, if it relies on bootstrapping starting with a system with a very large TCB at an earlier step. Then you have a large TCB that you trust only once; is this better than many smaller TCBs that you trust once each at each step of the process? (I'd believe it's easier to do, I just don't know if it's more trustworthy.) How does self-validation change that, if at all?

I would love a course like this one day. I hope you're right.

Talia

On Sat, Jan 8, 2022, 1:13 PM Adam Chlipala <adamc AT csail.mit.edu> wrote:

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