Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] A verified bootstrapping computer (academic curiousity)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] A verified bootstrapping computer (academic curiousity)


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.19+.

Top of Page