Re: Axiom Sane musings (SEL4)

Tim,

I can see how you can prove individual algorithms correct and I can see 
how you can use a proven Lisp but, if you want to prove "down to the 
metal", it looks to me like there is an enormous gap in-between which is 
SPAD.

Can you really prove SPAD correct?

You mention a specification language (PART 5) and a theorem language 
(PART 6) and presumably these will be mapped into SPAD somehow but does 
that really get to the root of a lot of the bugs in Axiom?

Theoretically the SPAD compiler is deterministic but for all practical 
purposes it doesn't seem to be. I suspect that, even for experts like 
yourself, it would be virtually impossible to predict what it will do. 
Is it possible to write a formal specification of the SPAD language 
syntax, semantics and its type system? Can it contain contradictions 
such as a type of all types?

I suspect that its would also be massively difficult (bordering on 
impossible without massive resources) to prove these sort of things in 
Idris but I still think it would be orders of magnitude easier than SPAD.

Martin

On 22/09/2019 01:22, Tim Daly 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 <[email protected]> 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 <[email protected]> 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
>>> [email protected]
>>> https://lists.nongnu.org/mailman/listinfo/axiom-developer
>>
> 

_______________________________________________
Axiom-developer mailing list
[email protected]
https://lists.nongnu.org/mailman/listinfo/axiom-developer