coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Freek Wiedijk <freek AT cs.ru.nl>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] A verified bootstrapping computer (academic curiousity)
- Date: Mon, 10 Jan 2022 11:11:32 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=freek AT cs.ru.nl; spf=Pass smtp.mailfrom=freek AT cs.ru.nl; spf=Pass smtp.helo=postmaster AT smtp1.science.ru.nl
- Ironport-data: A9a23:N9+tUK14jpPWR7vYlPbD5XRzkn2cJEfYwER7XOPLsXnJgj0khmNRmGJKXT2AaKyNMGCgetp/bom19h5QvZWGndMSHQtv/xmBbVoa8JufXYzxwmTYZn7JcJWbFCqL1yivAzX5BJhcokT0+1H9YtANkVEmjfvSHuOlULadUsxMbVYMpBkJ2UoLd9ER2dYAbeiRW2thiPuqyyHtEAfNNw1cbgr435m+RCZH55wejt+3UmsWPpintHeG/5Uc4Ql2yauZdxMUSaEMdgK2qnqq8V23wo/Z109F5tKNibPnahRMWbXTMA6FhzxMRu6khnCupARrif99baVALx4JzWzVxLidy/0V3XC0YQkzM6DPsO8GFQNFVSd6VUFD0Oabfyji7Z3Pp6HBWyG1ma00UCnaJ7Yw8eFuRGpK6PYwMyEIdhnFhuSswbv9RPMEuyiJBKEHJ6sEv214lHfCBvcrR5vOBb/Xo9lctArcT/tmRZ72D/f1oxI1BPgBX/FOBrvTIIk7gP/xwGL0cjBeo1/Tv7dx5Wy7IMlZzu32KNSMEjCVbZw9o6pajjuuE6fF7tUyP8fZ0yfD9HbEairng3bgQIxLfFGn3qcCvbBQr1D/zDUdTh2hvL+/jiZSnvo3x1M8okITkET5yKBnohQRkfF1TL5ocyPwg+ZtLtA=
- Ironport-hdrordr: A9a23:djWSEKrVoEP+dvl9WRikZ0saV5pMeYIsimQD101hICG9Ffb4qynOppomPHDP+VUssR0b6LK90cq7Lk80i6QU3WB5B97LN2PbUQCTQL2Kg7GO/wHd
- Ironport-phdr: A9a23:iKxkwR+sEnfyX/9uWRS8ngc9DxPPW53KNwIYoqAql6hJOvz6uci4ZQqGuK0m1QaBdL6YwsoMs/DRvaHkVD5Iyre6m1dGTqZxUQQYg94dhQ0qDZ3NI0T6KPn3c35yR5waBxdq8H6hLEdaBtv1aUHMrX2u9z4SHQj0ORZoKujvFYPekdm72/qv95DTfwlEiyexba5vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmhicJOSAk/m/UhMx/g75Urw+jqBNx2IPUfJ2ZOeBicq/BZ94WW2xMVdtRWSxbBYO8apMCAeobPelGsYb9pEYFohu/BQayGezvyz1Ihnzr1qA93eQhCx/J0xIjH98VrHvUt8/5NL0PUeyvyqnIySzOYvVL0jjy9IbGaAouoe2QXb1ua8rRz1EiGh3bgliTqIHrPzOY2/gQv2WH8uduWuaihnM6pwxtrDWhydkghIfHi48axV3I6Tl1zZs1K9C4VUJ2fdypHZpQuiycKoB4QdsiTnl1tCs017EKo4O3cSoFxZg92hLSauaLf5WH7x/tTOqcIil0iGhhdb+wnRq//0itxvfiWsWq01tHqDdOnMPWuXAXzRPT79CKSvtj8Uel3jaCzxvT6uRYIUAsiKbXMYUhzaIxlpUNt0TMAjH5lF/sjK+LbEkk/Oyo5/zmYrXguJCcK5d5hhzwP6gzgMCzHOY1PwcUU2SG+OmwzqDv8EL3TblSi/05iKjZsJTUJcQBoa65BhdY0og56xmhETim088VkmUcLF5fYhKHkpLlO1fKIPzgF/ewn0yskCt3x/DBJrDuHpLNLmHanLj9ebZ99lVTxREozdFf4pJUEqsOLOjyWk/3rtzYDwU2Pxa6w+b9W51B0dYVXnvKCauEOovTt0WJ76QhObqifogQ7RjnJvUmr8HvgHM4m1xVKaez0JYUQHujWO57ZUOdNym/yuwdGHsH61JtBNfhj0ePBGY7j5eaRKcg/mh9E4mnAIHIS8a3nfqH2HXidnW5TmtdTEqRV3HsJdzssxIkYznUONInlDhWDdCc
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+.