> 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