The Coq mailing list

[Andrei Popescu <andrei.h.popescu AT gmail.com>]

I believe Magnus Myreen and collaborators have made important
methodological (and practical) progress on this topic, e.g.,
https://drops.dagstuhl.de/opus/volltexte/2021/13896/pdf/LIPIcs-ITP-2021-1.pdf
https://link.springer.com/article/10.1007%2Fs10817-015-9324-6

Best wishes,
Andrei

On Sat, Jan 8, 2022 at 7:21 PM Talia Ringer <tringer AT cs.washington.edu> wrote:
>
> 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
>>