[Axiom-developer] Axiom Sane musings (SEL4)

[Tim Daly]

https://www.youtube.com/watch?v=uLCqJLFP7f8

The above link is about SEL4, the proven kernel.
They have about 1 million lines of proof.

I've been looking at the issue of "proof down to the metal".
It seems that SEL4 will run on an ARM processor which
is the basis for the Raspberry PI. I have a PI and am looking
to boot SEL4.

There is also the proven lisp stack which I've previously
mentioned.

It seems that it may be possible (in the next hundred years?)
to have an Axiom image that proves the GCD algorithms all
the way to the metal.

The search continues...

Tim