coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "D. Ben Knoble" <ben.knoble AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] A verified bootstrapping computer (academic curiousity)
Date: Tue, 11 Jan 2022 11:45:57 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ben.knoble AT gmail.com; spf=Pass smtp.mailfrom=ben.knoble AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf1-f54.google.com
Ironport-data: A9a23:ZUIlCaNbk0iKksTvrR3GlsFynXyQoLVcMsFnjC/WdQW+hTkkgWdVymRJCmmEOPqKZmr0ct0kOY22oUoBsZbRv4NqS1BcGVNFHysb85KdbTi6Bh6tZH3KdpWroHqKXqzyU/GYRCwPZiKa9kfF3oTJ9yEmj/nRH+OkUoYoBwgoLeNaYHd54f5cs7Vh6mJYqYDR7zKl4bsekeWHULOW82Ic3lYv1k62gEgHUMIeF98vlgdWifhj5DcynpSOZX4VDfnZw3DQGuG4EgMmLtsvwo1V/kuBl/ssItask7K+dkNTB7CPYU6BjX1ZX6XkiR9HzsAw+vxjZbxMNAEO1WrPwowZJNZl7fRcTS8jM6uKm+IaWR1VOy57NKxCvrTAJBBTtOTKkhSdKyewmp2CC2lvZdFCkgptOklF8uVdIzQQZDiYlueuyfS6TPNtj4ItNqHW0Ck3rik1l3eGGa9zGdabV/+fvZkCjWZpkpsbRbCDc5VMQCRLRxHkTx1rG14xNIgaouaNkiCnJmQD7AqBzUYsy23azQg01La0ddSIJpqFQsJamkverWXDl1kVyyoybLS3oQdpOFr17gMOoc/6ZG7WPLix9/ovhFPKg2JOVFsZUly0pfT/gUm7Mz6aAyT45QJ2xZXeNmTyJjU+Y/F8iHGBtx8YHdFXFoXWLSmTn7HM7V/x6ncsF1Z8hR9PiCPybTMv316N2djuAFSDdZX9pW21rt+pkN95BcTZwaLuq8PJocvpLuQPeL0Osy8=
Ironport-hdrordr: A9a23:3B2afKxLdZMSYul+sKiKKrPwl71zdoMgy1knxilNoNJuE/Bw8Pre+sjztCWE7wr5PUtLpTnuAsS9qB/nmaKdpLNhXotLsmHdyReVxcJZnPbfKwSJIVyAygcl79YfT0EdMr3N5ClB/KLHCVKDYq8dKbC8mcjCuQ6d9QYOcegNUc5dBmxCe2Om+yNNKjWuLKBJZaa0145opyeAZX9SVciyHH8DNtKz3eHjpdbJYQMmGxVi0wWFjSqp5LnmeiLopSs2YndgwaoC7WOAqADy5ryiv/anjjfQ2nTe9Y4+oqqQ9vJzQOKNl+kIIXHXhgGkaJ8JYcz7gAwI
Ironport-phdr: A9a23:Dmr/ghBPCS3oiF8T0pKRUyQUaUMY04WdBeb1wqQuh78GSKm/5ZOqZBWZua80ygaUBs6Ks7ptsKn/i+jYQ2sO4JKM4jgpUadncFs7s/gQhBEqG8WfCEf2f7bAZi0+G9leBhc+pynoeUdaF9zjaFLMv3a88SAdGgnlNQpyO+/5BpPeg9642uys5pHfeRhEiTqzbL99KBi6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjE2/mHYiMx+gqxYrhy8uRJw35XZYJ2JOPdkYq/RYc8WSGhHU81MVyJBGIS8b44XAuYPM+hUtZT2qkYQohu4GAKiAeXvyjhTiX/yw6I23fkqHAbd0wM+GdICqnfUrNPyNKgJVeC60rLFzTrGb/xM2Df97JLEfQwmofGJRL99d9faxkYzGQ3flFqQtZDlMC2P1uQLq2WW7/dtWOyuhmMmtwx8vjmiyMkvh4TKmo4bxE7J+yp4zYs2K9C1SFJ3bNy6HZVQqy2XNIV4TM0tTWxouis0xKALtJimdyYJ0JQq3wDTZ+CDfoSS4R/uVPydLSp5iX9nYr6yhxm//E69wePmTMa0ykxFri9dn9nMqH8N0xvT59CCSvRn/0eh3S+D1wTd6u1ZOEw0m6rWJpE7zr4/kZoTtkvDHivol0nskKCWcUAk9vCp6+ThfLrmuoeRO5Fohgz6KKgjmcyyDf4lPgUPXWWX4+Sx2bL78U38WrpKj/k2kqfDsJDdIMQWvrW2DBFT0oo56Ba/CTCm388cnXYZN19FdxeHgJLoO1HKOvz3EfC/g1G0nDdx2//GJqHhAonKLnXbjLjheq9951dAxwo30NBQ/IlZCqoBIfL2Qk/+rsbUDh4/MwyuwuboEs9x1o0EWTHHPqjMO6TL9FSM++gHIu+WZYZTtiyuBeIi4qukoTlxs1IbNYqv2pETZTrwSv5rJQOaZ33mhtopHmIDvw54R+vv3g7RGQVPbmq/CvpvrgowD5irWN+rrm+Fj7mI3SP9FZpTNDku4rGkFH7pc8CAVa5JZn/OZMBmlTMAWP6qTIpzjXlGUSf1zrNmKqzf/ShK7fre

On Tue, Jan 11, 2022 at 11:27 AM Timothy Carstens <intoverflow AT gmail.com>
wrote:
>
> I am reminded of the analogous question for metrology: starting from
> nothing, how do you build precise measurement tools?

Nothing to add on the Coq side, but this reminded me of "How Round is
Your Circle" by John Bryant, Chris Sangwin.

Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), (continued)
- 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