[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Axiom-developer] Axiom Sane musings (SEL4)
From: |
Tim Daly |
Subject: |
[Axiom-developer] Axiom Sane musings (SEL4) |
Date: |
Fri, 20 Sep 2019 01:56:46 -0400 |
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] Axiom Sane musings (SEL4),
Tim Daly <=
- Re: [Axiom-developer] Axiom Sane musings (SEL4), Henri Tuhola, 2019/09/20
- Re: [Axiom-developer] Axiom Sane musings (SEL4), Tim Daly, 2019/09/20
- Re: [Axiom-developer] Axiom Sane musings (SEL4), Henri Tuhola, 2019/09/20
- Re: [Axiom-developer] Axiom Sane musings (SEL4), Tim Daly, 2019/09/20
- Re: [Axiom-developer] Axiom Sane musings (SEL4), Martin Baker, 2019/09/21
- Re: [Axiom-developer] Axiom Sane musings (SEL4), Henri Tuhola, 2019/09/21
- Re: [Axiom-developer] Axiom Sane musings (SEL4), Martin Baker, 2019/09/21
- Re: [Axiom-developer] Axiom Sane musings (SEL4), Tim Daly, 2019/09/21
- Re: [Axiom-developer] Axiom Sane musings (SEL4), Martin Baker, 2019/09/22
- Re: [Axiom-developer] Axiom Sane musings (SEL4), Tim Daly, 2019/09/22