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 
    < Chronological >      < Thread >
  • From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] A verified bootstrapping computer (academic curiousity)
  • Date: Tue, 11 Jan 2022 13:50:16 +1100
  • Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
  • Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=WSUQO21gfnYrDSkOY4cdMeWOzwWRNd0W20u4v29uJYM=; b=ZPOIDgNqAVeOWakRVw+OovLKS1FgBbiPPaCLTSevqdNB5ctbzPHDjy0j4WwphqrG64+GH5jUKH7jKQtsS+dCk9GhMvjUaEptQuYwSnYj+DZMdxEU2I7G6gBOm6m7XKa/0r0biZXH3NuEZcH1D4T2TbOwTW5PXDv3/MycX15xTrUZtlV9p9WAgkBkcUKl+y8gbUm2Zliu+IS+fUYLR2hHdFz76pCZvedRy4RWSaPnd0PS+k4V1mnqvmxswJt4YJ0q2tKdvuy7PxtpE8EpzN4dIVEmf6v+Xp8BMfAEey/tWNkMrsqMHO5a6ETXzPlkizAit2l+7L7IZst8uC8aCFNcFA==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=LDLqTHPev4IhL/ZilQJ4QrM2Tjk50wwRvUnEOyoKn04/u+Ze2bZEOHjsj210jD/aQkirN8NQS0ThIezLlzp4LsbsGt9y814D4A/YJBqt81zDEpUjuRbfkxmUwKUMEKTCKpuUCbm2dnY088G5UhydDXCOQVzO1lvjbuReKzaLuyd7yuy5pdUlnbI41EjhF6dCk5i/q6Ka/ZWowW7h0YHpAtSBLQcMb7FYzHSArjZIFMfDNyYxmBzJO6pjeq333dmdtBUGq+e/bQjQ6Veg12E4kI0ygtx68PuYFnRxcm/trlus8meUdu0a8LHn8VcOKx4mXH22OnPyYAuvFdfuqBsd1A==
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME3-obe.outbound.protection.outlook.com
  • Ironport-data: A9a23:AV5Gr6O3fABdmezvrR2ZlsFynXyQoLVcMsFnjC/WdQXr0D4r0D0FzDQbWWmFaPePamP2eth1PIW2ox5QsJHTv4NqS1BcGVNFHysb85KdbTi6Bh6tZH3KdpWroHqKXqzyU/GYRCwPZiKa9kfF3oTJ9yEmj/nRH+KkU4YoBwgoLeNaYHd54f5cs7Vh6mJYqYDR7zKl4bsekeWHULOW82Ic3lYv1k62gEgHUMIeF98vlgdWifhj5DcynpSOZX4VDfnZw3DQGuG4EgMmLtsvwo1V/kuBl/ssIvqYqe6iN2gnGfvVNwXIjWdKUa+/hBQEvjY1zqswKPsbbwFQlimNmNdyjt5KsPRcSy91ZuuVwLtbCkEIVXAvVUFF0OevzXyXk8GJwkjXNVfl3O5pCmk/O5Be9+pqR2hTnRAdAGpWME/c3LveLLWTEbA33ZtLwNPQFIgYozRrySzTJe03RIjKBaTM/95Rmjkq7v2it97KP59CL2d7NUGYJUVbYAJPTshjwrm83SynNWBM9we8u4wc5k7/zChQ2Z7RKvzre/meHJ0AxALCsgoq5Ez8CxAecdmSkjOY6Sr1gemVxXKqHoUPCLe/6/hmxkWJwXAeAwEXUl39puSljkm5WJRULEl8x8bnloBqnGTDczU3d0TQTL+4Uh8gtx54OtABsFjI74ePpgGTCy4DUyJLb8EguIkuXzs221SVntTvQztyrLmSTnHb/bCRxd93ETZANncMPEfoUiNci+QPYqlq5v4McjqnOKezk5v4FSy2yi3iQO0WmeAIlcBSv0mk1Qmvvt9vz6QliiY84BiRU264qApkDGJgT+RE9nCDhct9wE2lopVtcZTKdwVyLAzDMH1VqBGwfQ==
  • Ironport-hdrordr: A9a23:/EvR46quEg2YJgvwVfpniUwaV5u6L9V00zEX/kB9WHVpm5Oj+vxGzc5w6farsl0ssREb9uxoS5PwJU80kqQFm7X5XI3SJzUO3VHFEGgM1/qA/9SNIVyGygcZ79YZT0EcMqyOMbEZt6bHCWCDer5PoeVvsprY49s2p00dMT2CAJsQijuRZDzrdXGeCDM2Z6bQQ/Gnl7d6TnebCDwqR/X+IkNAc/nIptXNmp6jSRkaByQ/4A3LqT+z8rb1HzWRwx9bClp0sP0f2FmAtza8yrSosvm9xBOZ/2jP765OkN+k7tdYHsSDhuUcNz2poAe1Y4ZKXaGEoVkO0aqSwWdvtOOJjwYrPsx15X+UVmapoSH10w2l6zoq42+K8y7uvVLT5ejCAB4qActIgoxUNjHD7VA7gd162KVXm0qEqpt+F3r77WrAzumNcysvulu/oHIkn+JWpWdYS5EiZLhYqpFa1F9JEa0HADnx5OkcYaZT5fnnlbZrmG6hHjPkVjEF+q3vYp1zJGbLfqE6gL3V79AM90oJinfxx6Qk7wM9HdwGOt15Dt//Q9VVfYd1P7orhJJGdZk8qPSMexzwqDL3QRSvyAfcZeg600ykke+F3Fxy3pDmRLUYiJEomJ7GSjpjxBwPR34=
  • Ironport-phdr: A9a23:lNySeR8BV7nJp/9uWaa8ngc9DxPPW53KNwIYoqAql6hJOvz6uci4ZQqGuKwm3QeBdL6YwsoMs/DRvaHkVD5Iyre6m1dGTqZxUQQYg94dhQ0qDZ3NI0T6KPn3c35yR5waBxdq8H6hLEdaBtv1aUHMrX2u9z4SHQj0ORZoKujvFYPekdm72/qv95DTfglEiz6wba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmiykJODAk/m/JhMx+jKBUrw6uqRNw2IPUfIKYOeBicq/Bc94XR2xMVdtRWSxbBYO8apMCAe4fMuZCsYb9olsPpgawCwa2CuLv0ThIhnnr1qA91+ouDxvG0xIlH9MOqnjaos/6NakJUeCyyqnF1i/Mb/VL2Tvn9ofHbw0hreuWUrJtaMfcz1QkGAzZgFuKs4PlIy+V2foXs2id9+dtS+2ihnA6pw1tvzSixMYhhpXJi48U1lzJ6yp0zYkpKNC2VUN3fNypHIVOuyyYNYZ6X8cvT3xptSsn1LALu4O2cS4Xw5ok3x7Sc/OKf5SS7h7+SOqcIy10iG95dL+8nRq/9UytxvXiWsS1zFpHoC9InsTQun8R1hHe79WLRud480qjwzmC0gXe5vxaLU0yiKHVMYQuwqQqmZoWqUnDHjH5mEHxjKKOakgr9PWm5/j6brn/oZGSOIF5hhj5Mqs1hMOzG+M4MhUSX2eA/uS8ybvj8lDjTLVSlP02lbXZv47GKsQHp665BAlV3pwk6xaiEzem1NMYnX4ELF5fZB2HiI3pN0nPIPD+E/i/n0yhnTh3y/zcI7HtHpfAImLenLv9frtx8UpRxQ4rwdBa/Z1UC7UBIPzpWk/2sdzVFhs3PBKuw+n5DdV81pkSV2yVDa6XK6PStlmI6/k1LOmKeY8ZoijyJOU45/L0l3A5hEcRfbO10psPdHC4AvNmLl2Fbnrrm9cNCHsFvg4jTOPxk1CCSj5SZ3OqX60m/D07CYSmDZ3CRo+3mrCB0j27TdVqYTVNDUnJGnP1fa2FXe0NYWScOJxPiDsBAJqsUYIkxFmCvRDhzLwvesjZ4CAdpNTP3cdu4Ov7nBcvszF4EoKUzjfeHClPgmoUSmpuj+hEqktnxwLbuUCZq9VlLoQKotZkCUI9P5OayPFmAdfvXA6HZs2OVFutXtShB3c2U841xNgNJU16Hof75vgm9yOsHvkYm6HNDYFmqso0MFD4Ids7xnrbkqA83QBOfw==
I presume, trusted computing base. The bit that has got to work right. You design your software to make this as small and simple as possible.

Jeremy

On 11/1/22 12:49, Robert Solovay wrote:
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 <mailto: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