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 _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
