The Coq mailing list

[Timothy Carstens <intoverflow AT gmail.com>]

I am reminded of the analogous question for metrology: starting from nothing, how do you build precise measurement tools?

You may enjoy this video which gives an answer in the context of metalworking/machining: https://www.youtube.com/watch?v=gNRnrn5DE58

But if you are low on time, allow me to summarize:

In a metal shop, the foundation of measurement is a thing called a "surface plate." These plates have the characteristic property of being extremely flat (see ASME B89.3.7-2013.) You can use them to make straight edges; from there the world is your oyster.

How do you make a surface plate? There is a simple trick:

1. Take two surfaces and rub them together. If you are lucky they will both wind up flat, but in all likelihood one will wind up concave and the other convex.

2. Now grab a third surface and rub it with the other two.

3. Observe that, if you have 3 surfaces and you keep rubbing them in pairs, then all will wind up flat.

Step (3) requires some basic mathematical reasoning: draw the complete graph with 3 nodes and label them according to the following rules:

i. If a node is flat, then every adjacent node must also be flat

ii. If a node is concave (resp convex), then every adjacent node must be convex (resp concave)

Of course, for the complete graph with 3 nodes, the only labeling consistent with (i) and (ii) is the labeling where all nodes are flat.

Now I ask: what is the TCB for this procedure?

Clearly it must contain the geometric argument given above together with some empirical observations about the materials in question (i.e., granite works well, mud does not).

End of story, right? Well, not exactly. The missing piece: a machine for doing the rubbing!

If you want to make some surface plates then you need to actually do the rubbing. What exact motion should you use? How much force should you apply? How often should you swap the plates? How many iterations should you perform? And most importantly: how can you build a reliable rubbing machine if you don't yet have a reliable flat surface to base your measurements on?

Answer: you don't have to!

The rubbing procedure is robust enough that, even if poorly applied, it will still generally improve flatness. This means you can use a crappy rubbing machine to make crappy surface plates, which in turn can be used to make a less-crappy rubbing machine, which then can make less-crappy surface plates, etc. Indeed, this is how humanity got to where we are today.

But it also means the "TCB" is not a "base" as much as it is a "layer."

So too with computers, I would think.

On Tue, Jan 11, 2022 at 6:23 AM Freek Wiedijk <freek AT cs.ru.nl> wrote:

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