coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

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: Tue, 11 Jan 2022 15:22:43 +0100
Authentication-results: mail3-smtp-sop.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:1V6fj6wM43NYaQtFzml6t+dkxyrEfRIJ4+MujC/XYbTApDMggmRVyzYfWWiGa/jYZ2v2KI0lYIWw/RxSucTTzNQ1OVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA/3z27AsFehsJpPnjkrrYuiJQUVUj/nSHOKlUbecYEideCc9IMsfoUI78wIGqtUw6TSJK1vlVeLa+6UzCnf9s9JHGj58B5a4lf9alK+aVAX0EbAJTasjUFf2zxH5BX+ETE27ByOQroJ8RoZWSwtfpYxV8F81/z91Yj+kuq3+blVTBKXZPAWIgXcQQbXkhBwqSi4ai/1icqNDNQEO1XPQw4sZJNZl7fRcTS8nJKDBm8wWSF9CDmd4OcWq/ZedfSjk75XNp6HBWyG1ma00UCnaJ7Yw8eFuRGpK6PYwMyEIdhnFhuSswbv9RPMEuyiJBN2zad5Z4GU5mGmfVeJ8FMiFGvWUu8sDiW9229QRSN/AQeEcTxZvSjXJRSFVHENOUMdm2L+87pXkWyZdtErM47E84mXVxwE3yqWrNt69RzBDfu0N9m7wm44M1z2R7tAm2N2jJf6t6XewnraJhij6VYQZGfui67hshDV/A0QNXQYOWwLTTeaR0yaDtxB3ciT4ORbCaYA57wqxU5/7W3VUZVaa6wUEVYM4//ISsWmwJ2m93+pdLmMfCCRcLtoi3CPzbVTGyXfR9+7U6fdTXHF5hJ5TGnp4bd9/BMTNEVI/WA==
Ironport-hdrordr: A9a23:b4vLyagrfAvEL+C7XDGhL3j1eXBQX6d13DAbv31ZSRFFG/Fwwfre48jzsiWE7Qr5OUtQ++xoV5PqfZqxz/RICMwqU4tKdjOWwVdAVbsSlbcKoQeOJ8SOzJ8/6U4IScEXNDSzNzlHZKDBjTVQeOxB/DDoysyVbM7lvglQZDAvRaF8yg9zTiKWCUN7fwVfGZYiCd69y6N81kGdUEVSQMSnI3EPG8zOvNPGr57/fRIdGloGyCTmt0LT1JfKVzaZwzIXWHdpx6oj/mjOmxH44KKZv/mgzBi07R6v071m3PXg1/5KD4i0kc4XJj/w4zzYALhJavmtvC0RqOrq0U0tk9XHvlMBMq1ImhTsV1Dwjxvx/gHqlA807Xzvw0LduHP/oKXCNVQHIvsEq4JFVxPTr3EtpdRtlIBGzwuixuZqMS8=
Ironport-phdr: A9a23:L7WQzhPmS6XTyARxD5El6nYyDRdPi9zP1u491JMrhvp0f7i5+Ny6ZQqDv6wr1QKQFtSDo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9AdgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/6v95HJfglFhCexbbx2IRmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOTA5/m/Jl8J+j6xbrx29qBNiwYHbbpqYNOZicq7HYd8WWXBMUthXWidcAo28dYwPD+8ZMOhYtYnyuUUBrRijDgasBePg1CJHhn703a05zu8sFg/G3BY+EN0Qs3TZt8n6NLwIXeCv0anE1zPDb/dP1Dr79YPHfQwvr+uWUrJsbcre11MvFwXdg1iOt4DoPDKY2OQNvmWH8uZtSf+ihWEjpgxsvzSi2skhhIbXiowbxF3J+ip0zJopKdClSEB2YcOoHYdSuiybN4Z7RN4pTWJwuCsi17ELt4O3cDIXxJklyBPTceGLfomS7h7+W+ucLy90iXF7dL6lgxu//lKsx+P8W8WuzlpGsClIn9/RvX4XzRPT8NKISv5l80ehxzmP0wfT5/lfIUAxiarbM4MtzqQrlpUPsETMACn2l1nog6OMbEUk5/Kk6+LjYrn+p5+cMZF7ih3mP6gzlMGzHP40PhUMUmWU4+iwybzu8VfkTLhFgPA6iqzZv4rbJcQfqK65GQhV0oM75haxFTepzsoXnXocIV1ZYxKLlZLpO0zULPD+Cfezm06snytzx/DaIr3hBY3AIWTEkLf4ZLpy90pcyBcowt1E/JJVCrQBIOrpVUPrtdzYCAU5Mw2uzOr9BtV9zNBWZWXaCaiAdajWrFWg5+Q1IuDKapVGliz6Lq0L/fPjjjcGmFIRfKuqlc8Zcn21HdxtOAODfDzqhoFSQi8xogMiQbmy2xW5WjlJaiPqN0rdzio+FJr/S5zIR42ri7HHxjr9GJkEPwiu5XiHCjHyasOCX6VVAMp3CsR61CYZE76lGddJ6A==

Dear Sam,

> - "Trusted" hardware/software - the TCB - by contrast, is not
> formally verified to be correct. As such, a leap of faith is
> required in order for a person to trust that it will perform
> securely and correctly.

In the case of Coq often the OCaml system is taken to be
part of TCB in this sense. Now you can be almost sure that
software as big as OCaml has undetected bugs. So here is
a TCB that is very probably _not_ fully correct.

The trust then is that those bugs won't affect the correct
functioning of Coq, I guess. Which I feel one still can
be reasonably confident about.

Personally I find this kind of "trust" discussion not
very interesting. Before you know it, it degenerates into
philosophy :-)

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), 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