Re: [Axiom-developer] Axiom Sane musings (SEL4)

[Tim Daly]

Does the Idris code cover GCD for polynomials?


On 9/20/19, Henri Tuhola <address@hidden> wrote:
> You can already define and prove gcd in idris/agda/coq. It's not too hard
> either.
>
> This weekend I am trying to prove transitive closure can be computed in
> Idris. The way I represent it is that I have f:(a -> a -> Type), this forms
> a type that is inhabited when a statement is true. I can wrap this into
> another type that represents transitiveness. I can get (Transitive f x),
> from which I can make a set: (Set (Transitive f x)). This type describes a
> set containing all symbols reachable from 'x', through some way they relate
> 'f'.
>
> Idris has some flaws that annoy when using it. Those issues become clear
> when trying to prove injectivity for certain sort or functions that have
> multiple variables. Also it's sometimes quite dumb, forgetting how values
> computed too early and other times is remembers that quite too well.
>
> -- Henri Tuhola
>
> pe 20. syysk. 2019 klo 8.56 Tim Daly <address@hidden> kirjoitti:
>
>> 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
>> address@hidden
>> https://lists.nongnu.org/mailman/listinfo/axiom-developer
>>
>