Dear Boostrappable list,
a few months ago I presented here my project asmc[1], which is still
making progress. It is currently able to compile a patched and stripped
down version of iPXE, and so to have network drivers, starting from a 15
KiB seed booted directly from the BIOS.
[1] https://gitlab.com/giomasce/asmc
However, latest news is that, following an interesting conversation[2]
started by Mario Carneiro on the Metamath mailing list, it came to our
attention that an interesting combination of asmc and Metamath can be
devised, in order to strengthen both projects. The relevant part of the
conversation starts more or less at [3].
[2] https://groups.google.com/forum/#!topic/metamath/raGj9fO6U2I
[3] https://groups.google.com/d/msg/metamath/raGj9fO6U2I/QKB5zvCRBQAJ
For the context, Metamath is a mathematical formalization project,
already able to prove a relevant amount of mathematical theorems from
the set theory axioms. Asmc is a bootstrapping project that focuses on
running as early as (currently) possible in the computer boot chain to
minimize dependency on binary components. The idea is to use Metamath
(actually Metamath Zero, but the difference is not relevant is this high
level overview) to prove the correctness of the early stages of asmc,
and use asmc to run the Metamath verifier in the minimal execution
context possible, in order to minimize the assumptions required for the
proving process as much as possible. In other words, we would try to
verify and bootstrap both asmc and a Metamath Zero verifier at the same
time, so that trustworthiness of both is maximized.
This also means that asmc will be able to provide an even stronger
starting platform for other projects that will depend on it, as it
hopefully happen at some point for mes (janneke and I had a chat about
this during FOSDEM; there is still quite a long bridge to gap, but we
look for the future!).
Everything is still in very early stages, but I felt it was nice to
report here about this discussion. As usual, I am happy to receive
comments and (even better!) contributions.
Happy bootstrapping, Giovanni.
--
Giovanni Mascellani <g.mascellani@xxxxxxxxx>
Postdoc researcher - Université Libre de Bruxelles
Attachment:
signature.asc
Description: OpenPGP digital signature
