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: 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



Archive powered by MHonArc 2.6.19+.

Top of Page