Re: [open-axiom-devel] [Axiom-developer] Proving Axiom Correct

I was largely poking, tongue in cheek, at the earlier syllogism:

>> The point is that Lisp has a formal logic basis and, as Spad is really
>> just a domain specific language implemented in Lisp then Spad shares
>> the formal logic basis.

-- Gaby

On Thu, Jan 12, 2017 at 10:35 PM, Tim Daly <[email protected]> wrote:

> > There were implementations of C in Lisp. So C shares that formal logic
> basis, or that it was discovered?
>
> According to Wadler, C is an "invented" language, not a "discovered"
> language.
>
> Wadler (https://www.youtube.com/watch?v=aeRVdYN6fE8)  at around 40 minutes
> shows the logician's view versus the computer science view of various
> theories.
> He makes a distinction betwen invented and discovered langauges.
>
> (begin quote of Wadler)
>
> Every interesting logic has a corresponding language feature:
>
> Natural Deduction (Gentzen) <==> Typed Lambda Calculus (Church)
> Type Schemes (Hindley) <==> ML Type System (Milner)
> System F (Girard) <==> Polymorphic Lambda Calculus (Reynolds)
> Modal Logic (Lewis) <==> Monads (state, exceptions) (Kleisli, Moggi)
> Classical-Intuitionistic Embedding (Godel) <==> Continuation Passing
> (Reynolds)
> Linear Logic (Girard) <==> Session Types (Honda)
>
> Languages which were "discovered" (based on theory):
>
> Lisp (McCarthy)
> Iswim (Landin)
> Scheme (Steele and Sussman)
> ML (Milner, Gordon, Wadsworth)
> Haskell (Hudak, Hughes, Peyton Jones, Wadler)
> O'Caml (Leroy)
> Erlang (Armstrong, Virding, Williams)
> Scala (Odersky)
> F# (Syme)
> Clojure (Hickey)
> Elm (Czaplicki)
>
> At about minute 43 we hear:
>
> "Not all of these languages are based on lambda calculus ...
> but there is a core that is "discovered". Now most of you work
> in languages like Java, C++, or Python and those languages I will
> claim are not discovered; they are "invented". Looking at them
> you can tell they are invented. So this is my invitation to you
> to work in languages that are "discovered".
>
> Somebody asked before about "dependent types". It turns out that
> when you extend into dependent types you now get languages that
> have "for all" and "there exists" that corresponds to a feature
> called "dependent types". So this means that you can encode very
> sophisticated proofs, pretty much everything you can name as a
> program. And so the standard way to get a computer to check a
> proof for you and to help you with that proof is to represent that
> as a program in typed lambda calculus.
>
> All of these systems are based on a greater or lesser extent on
> that idea:
>
> Automath (de Bruijn)
> Type Theory (Martin Lof)
> Mizar (Trybulec)
> ML/LCF (Milner, Gordon, Wadsworth)
> NuPrl (COnstable)
> HOL (Gordon, Melham)
> Coq (Huet, Coquand)
> Isabelle (Paulson)
> Epigram (McBride, McKinna)
> Agda (Norell)
>
> (end quote)
>
> Axiom is using Coq for its proof platform because Axiom needs
> dependent types (e.g. specifying matrix sizes by parameters).
>
> In addition, Coq is capable of generating a program from a
> proof and the plan is to reshape the Spad solution to more
> closely mirror the proof-generated code. Also, of course, we need
> to remove any errors in the Spad code found during proofs.
>
> It seems there must be an isomorphism between Coq and Spad.
>
> At the moment it seems that Coq's 'nat' matches Axiom's
> NonNegativeInteger. Coq also has a 'Group' type which needs
> to be matched with the Axiom type. The idea is to find many
> isomorphisms of primitive types which will generate lemmas
> that can be used to prove more complex code.
>
> Given that Axiom has an abstract algebra scaffold it seems likely
> that a reasonable subset can be proven (modulo the fact that there
> are arguable differences from the abstract algebra type hierarchy).
>
> Currently Coq is run during the Axiom build to check any proofs
> of Spad code that are included. ACL2 is also run during the build
> to check any proofs of Lisp code that are included.
>
> I'm taking a course at Carnegie-Mellon this semester using Lean
> (a Coq offshoot) in order to try to make some working examples
> of proving Spad code correct.
>
>
> On Thu, Jan 12, 2017 at 10:14 PM, Gabriel Dos Reis <
> [email protected]> wrote:
>
>> There were implementations of C in Lisp. So C shares that formal logic
>> basis, or that it was discovered?
>>
>> On Wed, Jan 11, 2017 at 8:17 PM, Tim Daly <[email protected]> wrote:
>>
>>> I'm making progress on proving Axiom correct both at the Spad level and
>>> the Lisp level. One interesting talk by Phillip Wadler on "Propositions
>>> as
>>> Types", a very entertaining talk, is here:
>>> https://www.youtube.com/watch?v=IOiZatlZtGU
>>>
>>> He makes the interesting point late in the talk that some languages are
>>> "discovered" based on fundamental logic principles (e.g.Lisp) and others
>>> are "invented" with no formal basis (e.g. C). As he says, "you can tell
>>> whether your language is discovered or invented".
>>>
>>> The point is that Lisp has a formal logic basis and, as Spad is really
>>> just a domain specific language implemented in Lisp then Spad shares
>>> the formal logic basis.
>>>
>>>
>>>
>>> _______________________________________________
>>> Axiom-developer mailing list
>>> [email protected]
>>> https://lists.nongnu.org/mailman/listinfo/axiom-developer
>>>
>>>
>>
>

------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, SlashDot.org! http://sdm.link/slashdot

_______________________________________________
open-axiom-devel mailing list
open-axiom-devel-5NWGOfrQmneRv+LV9MX5uipxlwaOVQ5f@public.gmane.org
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel