Of particular interest is clarity. I've been working with LEAN. The code is in C++ and is very clever. For instance, there is a beautiful macro embedded in data structures to perform reference counting.
Unfortunately, I can't reverse-engineer the logic rules that are embedded in the C++ code. HOL, on the other hand, seems to have a very clear connection betwen the code and the logic rules. In a proof system it is vital that the logic rules and their implementation is "obviously correct" and transparent. I have not yet looked at Idris so I can't comment on that. Tim On 9/21/19, Tim Daly <axiom...@gmail.com> wrote: > Hmm. The problem to be solved involves several parts. > Idris is of interest in PART 6, 7, and 8 below. > > PART 1: We have the domain > > We have GCD in NAT (axiom: NonNegativeInteger or NNI) > > NonNegativeInteger is what Axiom calls a "Domain", which means > that it contains signatures, such as > > quo : (%,%) -> % > rem : (%,%) -> % > gcd : (%,%) -> % > > which says that gcd takes 2 NonNegativeIntegers (NATs) and > returns a NonNegativeInteger (NAT). > > The NonNegativeInteger domain also includes information about > how its elements are represented. > > PART 2: We have an implementation of gcd in the domain > > The NNI domain contains an implementation of gcd: > > gcd(x,y) == > zero? x => y > gcd(y rem x,x) > > PART 3: We have a way to inherit things for the domain > > The NNI domain inherits properties from what Axiom > (unfortunately) calls Categories. Categories provide > additional signatures and default implementations. > > PART 4: We have the FUNDAMENTAL PROBLEM > > The PROBLEM to be solved is that we want to prove > that the above code for gcd is correct. > > Of course, the first question is "correct with respect to..." > > PART 5: We need a specification language > > There needs to be a specification of the gcd function. > What are the properties it should fulfill? > What are the invariants? > What are the preconditions? > What are the postconditions? > > Some parts of the specification will be inherited. > > Which means we need a language for specification. > > PART 6: We need a theorem language > > Given a specification, what theorems are available? > Some theorems are inherited from the categories, > usually as axioms. > > Some theorems and axioms are directly stated in > the NNI domain. > > Some lemmas need to be added to the domain to help > the proof process. > > Which means we need a language for theorems. > > PART 7: We need a proof engine > > Now that we have an implementation, a specification, > a collection of theorems and pre- and post-conditions, > lemmas, and invariants we need a proof. > > Which engine will we use for the proof? > What syntax does it require? > Does it provide a verifier to re-check proofs? > > PART 8: We need to prove many GCD algorithms > > Axiom contains 22 signatures for gcd. For example, > it contains a gcd for polynomials. The above machinery > needs to support proofs in those domains also. > > PART 9: LOOP > > GOTO part 4 above, pick a new function, and repeat. > > > PART 10: ISSUES > > PART 10a: "Down to the metal" > > THere are a pile of "side issues". I'm re-implementing Axiom > using Common Lisp CLOS. THe defclass macro in CLOS > creates new Common Lisp types. This allows using the types > for type-checking (currently looking at bi-directional checking > algorithms) > > Axiom sits on Common Lisp. There is a question of using a > "trusted core". I'm looking into Milawa > https://www.cl.cam.ac.uk/~mom22/soundness.pdf > with a deeply layered design. > > I'm also looking at SEL4 on ARM > https://ts.data61.csiro.au/publications/nicta_full_text/3783.pdf > which is a trustworthy operating system. > > I wrote a paper on the semantics of the Intel instruction set: > Daly, Timothy Intel Instruction Semantics Generator SEI/CERT Research > Report, March 2012 > http://daly.axiom-developer.org/TimothyDaly_files/publications/sei/intel/intel.pdf > so SEL4 on Intel is interesting. > > > PART 10b: Dependent type theory > > Dependent types are undecidable. Axiom contains several > heuristics to resolve types at runtime. The heuristic type > algorithm needs to be explicit and declarative. > > PART 10c: Size > > Axiom contains about 10,000 algorithms in 1100 categories, > domains, and packages. This is going to take a while. > > PART 10d: Mathematics > > Many of the algorithms are partial. Many are PhD thesis > work (and hard to understand). Many are ad hoc and have > no mathematical specification. > > PART 10e: Time > > The target delivery date is April, 2023. > There is much to do. > > Tim > > > On 9/21/19, Henri Tuhola <henri.tuh...@gmail.com> wrote: >> Idris has a way to present equalities like this: >> >> addition_unit : (a:Nat) -> (a + 0) = a >> addition_s : (a,b:Nat) -> (a + S b) = S (a + b) >> add_commutative : (a,b:Nat) -> (a + b = b + a) >> >> They can be used to prove more things: >> >> try_out : (x,y:Nat) -> ((x + 0) + y) = y + x >> try_out x y = rewrite addition_unit x in add_commutative x y >> >> It's rewriting the left expression to right expression, though you can >> easily flip the direction. For clarity I show these few dissections: >> >> try_out x y = ?a1 >> a1 : plus (plus x 0) y = plus y x >> >> try_out x y = rewrite addition_unit x in ?a2 >> a2 : plus x y = plus y x >> >> Idris has this feature called "Elaborator reflection". It allows you >> to describe automated tactics for writing proofs/programs. >> The "getGoal" and "getEnv" allow you to examine types in the context: >> >> getGoal : Elab (TTName, TT) >> getEnv : Elab (List (TTName, Binder TT)) >> >> The elaborator reflection also allows accessing the term rewriting. I >> suppose that's all you need in order to write a program that >> simplifies equations inside the type context? >> >> -- Henri Tuhola >> >> On Sat, 21 Sep 2019 at 11:50, Martin Baker <ax87...@martinb.com> wrote: >>> >>> I'm a fan of both Axiom and Idris. I think my ideal would be Axiom >>> mathematics build on top of the Idris type system. >>> >>> The Axiom type system was incredibly advanced for its time but I suspect >>> the Idris type system has finally caught up and overtaken it? Correct me >>> if I'm wrong but I think the Axiom type system does not have the >>> following capabilities that Idris does: >>> >>> * Enforcement of pure functions. >>> * Ability to flag a function as total as opposed to partial (automatic >>> in some cases). >>> * Universes (types of types hierarchy). >>> >>> I'm no expert but I would have guessed these things would be almost >>> indispensable for proving Axiom correct? >>> >>> Also Idris makes it far more practical to use these things, I don't >>> think Axiom can implement category theory constructs like monads. Also, >>> although both have dependent types, Axiom does not use them for say, >>> preventing the addition of a 2D vector to a 3D vector. In Idris this is >>> more likely to be compile time error than a runtime error, I know there >>> are theoretical limits to this but I think Idris has capabilities to >>> make this practical in more cases. >>> >>> I don't pretend I know how an Idris type system could be used with Axiom >>> in practice. For instance I think the proofs Henri is talking about are >>> equalities in the type system (propositions as types). So how would >>> these equations relate to equations acted on by equation solvers (which >>> might be an element of some equation type). Could there be some way to >>> lift equations into the type system and back? >>> >>> Sorry if I'm confusing things here but I just have an intuition that >>> there is something even more powerful here if all this could be put >>> together. >>> >>> Martin >>> >>> On 21/09/2019 04:28, Tim Daly wrote: >>> > Axiom has type information everywhere. It is strongly >>> > dependently typed. So give a Polynomial type, which >>> > Axiom has, over a Ring or Field, such as >>> > Polynomial(Integer) or Polynomial(Fraction(Integer)) >>> > we can use theorems from the Ring while proving >>> > properties of Polynomials. >>> >>> _______________________________________________ >>> 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