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