axiom-developer
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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


From: Tim Daly
Subject: Re: [Axiom-developer] Axiom Sane musings (SEL4)
Date: Sun, 22 Sep 2019 14:00:37 -0400

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 <address@hidden> 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 <address@hidden> 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 <address@hidden> 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
>>> address@hidden
>>> https://lists.nongnu.org/mailman/listinfo/axiom-developer
>>
>



reply via email to

[Prev in Thread] Current Thread [Next in Thread]