You can already define and prove gcd in idris/agda/coq. I=
t's not too hard either.

This weekend I am trying to prove transi=
tive closure can be computed in Idris. The way I represent it is that I hav=
e f:(a -> a -> Type), this forms a type that is inhabited when a stat=
ement is true. I can wrap this into another type that represents transitive=
ness. I can get (Transitive f x), from which I can make a set: (Set (Transi=
tive 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 qui=
te dumb, forgetting how values computed too early and other times is rememb=
ers that quite too well.

-- Henri Tuhola

pe 20. syysk. 2019 klo 8.56 Tim Daly <=
axiomcas@gmail.com> kirjoitti:

https:/= /www.youtube.com/watch?v=3DuLCqJLFP7f8--0000000000006660860592fb629c-- From MAILER-DAEMON Fri Sep 20 12:37:35 2019 Received: from list by lists.gnu.org with archive (Exim 4.90_1) id 1iBLuZ-0004GP-KC for mharc-axiom-developer@gnu.org; Fri, 20 Sep 2019 12:37:35 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:55899) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from

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".<= br> 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