> This technically also means we have to trust the hardware, OS, OCaml compiler that the Rocq proof checker relies on.
It just so happens Claude and I recently did an independent implementation of OCaml and ruled out malware in the compiler bootstrap via DDC (and also by achieving byte identical outputs).
So, we can at least rule out "trusting trust" malware in the OCaml part of the stack and up. (Rocq does not have trusting trust concerns since it's implemented in OCaml and C)
> This technically also means we have to trust the hardware, OS, OCaml compiler that the Rocq proof checker relies on.
It just so happens Claude and I recently did an independent implementation of OCaml and ruled out malware in the compiler bootstrap via DDC (and also by achieving byte identical outputs).
https://discuss.ocaml.org/t/ocaml-compiler-implemented-in-c-...
So, we can at least rule out "trusting trust" malware in the OCaml part of the stack and up. (Rocq does not have trusting trust concerns since it's implemented in OCaml and C)