coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Robert Solovay <solovay AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] A verified bootstrapping computer (academic curiousity)
- Date: Mon, 10 Jan 2022 17:49:53 -0800
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=solovay AT gmail.com; spf=Pass smtp.mailfrom=solovay AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f180.google.com
- Ironport-data: A9a23:07jO/KgUZWzPQYhJG6b3LI1qX161AxEKZh0ujC45NGQNrF6WrkUEzzdKWziFO6mONGv2Ldl/Pd+/o00Bv8eHyYNkGwttqlhgHilAwSbnLYTAfx2oZ0t+DeWaERk5t51GAjX4wXFdokb0/n9BCZC86yksvU20buCkUrScY3kpHVQMpBoJ0HqPpcZp2uaEvvDiW2thifuqyyHuEAfNNwxcagr42IrfwP9bh8kejRtD1rAIiV+ni3eF/5UdJMp3yahctBIUSKEMdgKxb76rIL1UYgrkExkR5tONyt4Xc2UPS7/WeAmK0z9YAvj6xBdFoSM23+AwM/90hUV/0W3Y2YAsjowT69rpGV9B0q7kwIzxVzFDFCV5I6RX0LDCKHm798eUyiUqdlO2mKs1VBFnVWEf0r8vXTsmGeYjADsKd1WIg/+86KmqT/FlwMUlNsjieo0F0kyMZxnNVaN8B8/XGvCSo4dMhmJowJofTK/KPJ9BL2d7M0HpfTlkP3M7CLYflcGUnF3BchhM8QrA/PNzuXy7IBdZ1bHsNJ/UfoXPS5wFxgCXoWXJ+2m/CRYfXOFzAAGtqhqE7tIjVwuiMG7TKFG5yhKuqFiax2hWCRlPEFXi8aH/hUm5VNZSbUcT/0LCaIBaGFODFrHAs9+Q+RZofSLwn/JfFuQ77EeGza+8D8OxGD0fVjAYADA5nJZeeNHpv2NlW/vmADVutPueTnf1GnK8xd+tEXB9EFLurhPogefIDxcPbW3zYt/yog5fLZOI
- Ironport-hdrordr: A9a23:fFH216DM0O+Q0RzlHemV55DYdb4zR+YMi2TDtnoBMCC9F/bzqynApoV/6faZskdyZJhko6HiBEDiexLhHPxOkO0s1N6ZNWGMhILrFuFfBODZslrd8kPFh4hgPGRbH5SWyuecMbG3t6nHCcCDfeod/A==
- Ironport-phdr: A9a23:+hKUSRfF7AvYct0vgnzdLVF6lGM+j97LVj580XLHo4xHfqnrxZn+JkuXvawr0AWQG9yGsrkV06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHNfglEniexbLNvIBm5qQjdqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W7YhMx/jqJVrhyiqRJi3YDbfJqYO+Bicq7HZ94WWXZNU8RXWidcAo28dYwPD+8ZMOhEqInyvEUBrQGiBQKxGe3vzTtIhnjo3aIg0+UqDAbL3BcnH9IKt3TUss/6NacJXOC6yanH1zTDb/dM1Tjh74jIdwksrPeRVr1/bcTf01MgFx/ZjlqOs4zlOSuY2/oTvmab4ORtSfyjhnMmpgx/rTaix8Mhh5XGiI4I113I6yV0zYcpKdO2RkN3fd6qHZ9TuiyeOYZ7TcIvT310tSs817YIuoa7cTAUxJg7wxPTcf+KfoiS7h7+VeucIC10iG9mdb6jgRu57FKuxffmVsau1VZHtipFncfItnAKzxHT79KISvp5/ku42DaP0x3f5vhKIUwplqfXN4QtwrE3lpoUvkTDGjH5lF/qg6+Rc0Uo4umo6+L5bbX6vpKQKZN4hwXkPqktmsGzG/k0PwkPUmSB5Oix16Hv8VX8QLpQj/02lqfZsIrdJcQevqO5GAhV0oIk6xahFTin0M8VnXYCLF1feRKHi5LlNE3JIPD9Ffu/mUijkC93x/DaOb3sGonCLn/akLv4Ybl971NcxxEowNBE55NUD6kBL+jpVk/wstzYFB45PBauz+bpEtUunr8ZDGmIG+qSNL7YmV6O/OMmZeeWN6EPvzOoEf8v6uTyxUQ+nVgDdLjhiYAQbHemF+VOLECQYH6qidAERzRZ9jEiRfDn3QXRGQVYYGy/CvpUDtQTB4evDIOFTYeo0uTpNMaTG5RXYiVHDgnJHy64L8OLXPADbC/UKchkwGRsvVeJRIoo1BXovwj/meMPEw==
What, precisely, does TCB mean in these letters?
Thanks,
Bob Solovay
On Mon, Jan 10, 2022, 2:12 AM Freek Wiedijk <freek AT cs.ru.nl> wrote:
Hi Talia,
>What is the smallest you can get the TCB [...] in the end?
What should be considered part of the TCB (even if it's
not code) is the explanation _why_ the TCB is the TCB.
If I give you a huge repo with a lot of code, then point
at some files and tell you "that's the TCB", there really
needs to be some explanation why that is the case.
Freek
- [Coq-Club] A verified bootstrapping computer (academic curiousity), Talia Ringer, 01/08/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Adam Chlipala, 01/08/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Talia Ringer, 01/08/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Andrei Popescu, 01/08/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Marco Servetto, 01/08/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Talia Ringer, 01/08/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Sam Kuper, 01/09/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Freek Wiedijk, 01/10/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Robert Solovay, 01/11/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Jeremy Dawson, 01/11/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Sam Kuper, 01/11/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Freek Wiedijk, 01/11/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Timothy Carstens, 01/11/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), D. Ben Knoble, 01/11/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Timothy Carstens, 01/11/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Freek Wiedijk, 01/11/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Sam Kuper, 01/11/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Jeremy Dawson, 01/11/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Robert Solovay, 01/11/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Adam Chlipala, 01/08/2022
Archive powered by MHonArc 2.6.19+.