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 <axiom...@gmail.com> 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 < > g...@integrable-solutions.net> 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 <axiom...@gmail.com> 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 >>> 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
