I'm makin=
g progress on proving Axiom correct both at the Spad level and

th=
e Lisp level. One interesting talk by Phillip Wadler on "Propositions =
ashttps://www.youtube.com/watch= ?v=3DIOiZatlZtGU

whether your language is discovered or invented".

just a domain specific language implemented in Lisp then Spad shares

<= /div>the formal logic basis.

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 Dal=
y <axiomcas@gmail.com> wrote:

the formal logic basis.just a domain specific language implemented i= n Lisp then Spad sharesThe point is that Lisp has a formal logic basis an= d, as Spad is reallywhether your language is discovered or inve= nted".are "invented" with no formal basis (e.g. C). As he sa= ys, "you can tell"= discovered" based on fundamental logic principles (e.g.Lisp) and other= sHe makes the = interesting point late in the talk that some languages areI'm = making progress on proving Axiom correct both at the Spad level andTypes", a very entertaining talk, is here:

the Lisp level. One interesting talk by Phillip Wadler on "Proposit= ions as

https:= //www.youtube.com/watch?v=3DIOiZatlZtGU

_______________________________________________

Axiom-developer mailing list

Axiom-developer@nongnu.org

https://lists.nongnu.org/mailman/lis= tinfo/axiom- developer

> 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 &quo=
t;discovered" language.

shows the logician's =
view versus the computer science view of various theories.(begi= n quote of Wadler)

Every interesting logic has a corresponding langu= age feature:

Natural Deduction (Gentzen) <=3D=3D> Typed Lambda= Calculus (Church)

Type Schemes (Hindley) <=3D=3D> ML Type System = (Milner)

System F (Girard) <=3D=3D> Polymorphic Lambda Calculus (R= eynolds)

Modal Logic (Lewis) <=3D=3D> Monads (state, exceptions) (= Kleisli, Moggi)

Classical-Intuitionistic Embedding (Godel) <=3D=3D>= ; Continuation Passing (Reynolds)

Linear Logic (Girard) <=3D=3D> S= ession Types (Honda)

Languages which were "discovered" (ba= sed on theory):

Lisp (McCarthy)

Iswim (Landin)

Scheme (Steele = and Sussman)

ML (Milner, Gordon, Wadsworth)

Haskell (Hudak, Hughes, P= eyton Jones, Wadler)

O'Caml (Leroy)

Erlang (Armstrong, Virding, W= illiams)

Scala (Odersky)

F# (Syme)

Clojure (Hickey)

Elm (Czapli= cki)

At about minute 43 we hear:

"Not all of these langu= ages are based on lambda calculus ...

but there is a core that is "= discovered". Now most of you work

in languages like Java, C++, or P= ython and those languages I will

claim are not discovered; they are &quo= t;invented". Looking at them

you can tell they are invented. So thi= s 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 language= s that

have "for all" and "there exists" that corres= ponds to a feature

called "dependent types". So this means tha= t you can encode very

sophisticated proofs, pretty much everything you c= an 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 <= br>as a program in typed lambda calculus.

All of these systems are = based on a greater or lesser extent on

that idea:

Automath (de B= ruijn)

Type Theory (Martin Lof)

Mizar (Trybulec)

ML/LCF (Milner, G= ordon, Wadsworth)

NuPrl (COnstable)

HOL (Gordon, Melham)

Coq (Huet= , Coquand)

Isabelle (Paulson)

Epigram (McBride, McKinna)

Agda (Nor= ell)

(end quote)

Axiom is using Coq for its proof platform be= cause Axiom needs

dependent types (e.g. specifying matrix sizes by param= eters).

In addition, Coq is capable of generating a program from a <= br>proof and the plan is to reshape the Spad solution to more

closely mi= rror the proof-generated code. Also, of course, we need

to re=
move any errors in the Spad code found during proofs.

It = seems there must be an isomorphism between Coq and Spad.

At the mome= nt it seems that Coq's 'nat' matches Axiom's

NonNegative= Integer. Coq also has a 'Group' type which needs

to be matched w= ith the Axiom type. The idea is to find many

isomorphisms of primitive t= ypes which will generate lemmas

that can be used to prove more complex c= ode.

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 abstrac=
t algebra type hierarchy).

Currently Coq is run during th= e Axiom build to check any proofs

of Spad code that are included. ACL2 i= s also run during the build

to check any proofs of Lisp code that are in= cluded.

I'm taking a course at Carnegie-Mellon this semester usi= ng Lean

(a Coq offshoot) in order to try to make some working examples

On Thu, Jan 12, 2017 at 10:14 PM, Gabriel Dos Reis <=
span dir=3D"ltr"><gdr@integrable-solutions.net> wrote:

There were implem=
entations 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 <=
axiomcas@gmail.com> wrote:

______________________________the formal logic basis.just a domain specific language implemented in Lisp then Spad s= haresThe point is that Lisp has a formal logic basis and, as Spad is real= lywhether your language is discovered or invented".are &qu= ot;invented" with no formal basis (e.g. C). As he says, "you can = tell"discovered" b= ased on fundamental logic principles (e.g.Lisp) and othersHe makes the interesting point = late in the talk that some languages areT= ypes", a very entertaining talk, is here:I'm making progress on= proving Axiom correct both at the Spad level andthe Lisp level.= One interesting talk by Phillip Wadler on "Propositions as

https://www.youtube.com/= watch?v=3DIOiZatlZtGU _= ________________

Axiom-developer mailing list

Axiom-devel= oper@nongnu.org

https://lists.nongnu.org/mailman/listi= nfo/axiom-developer

>From: Kurt Pagani <nilqed@gmail.com>

>

>>

&g= t;> 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.

= >

>A SPAD extractor should be feasible but it may take some time t= o set up the

>necessary infrastructure to compile a plugin. E.g. see<= br>>

>https://github.com/coq/coq/tree/trunk/plugins/extraction

I had not actually thought of trying to extract Spad directly.>

>>

&g= t;> 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.

= >

>A SPAD extractor should be feasible but it may take some time t= o set up the

>necessary infrastructure to compile a plugin. E.g. see<= br>>

>https://github.com/coq/coq/tree/trunk/plugins/extraction

<= /div>My plan was to extract the ML code and compare it to Spad.

It would be interesting to extract Spad directly.

Indeed it would pro= bably uncover bugs in Axiom's compiler.

I think it w=
ould be really valuable to try to converge Spad and COQ.

It w=
ould force more functional programming discipline on Spad code.

>There is a recent post @ https://news.ycombinator.c= om/item?id=3D12183095

>about Coq2Rust where I saw some nice ideas= :

>

>-- https:= //github.com/pirapira/coq2rust

>

>There's more about it= if you use the search field (bottom) at

>https://news.ycombinator.com/news.

>

>&g= t;

>> It seems there must be an isomorphism between Coq and Spad.=

>>

>> At the moment it seems that Coq's 'nat= 9; 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 cod= e.

>>

>

>Still there are a lot of Lisp dependencies, = e.g. integer.spad

>

>zero? x =3D=3D ZEROP(x)$Lisp

>--=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0 one? x =3D=3D ONEP(x)$Lisp

>=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 one? x =3D=3D x =3D 1

>=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0 0 =3D=3D 0$Lisp

>=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0 1 =3D=3D 1$Lisp

>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0 base() =3D=3D 2$Lisp

This proof effort uses COQ for the Sp= ad code and ACL2 for the Lisp code.

We will probably need a COQ.Lisp int= erface package that provides proofs

of Axiom's $Lisp package calls. = This needs to be formalized anyway. There

should be a complete list made= .

At the moment (in book volume 5) there is a chapter that contains = the Lisp

code that Axiom uses but it does not cover direct lisp package = calls like 0$Lisp.

I''ll try to collect all instances and docume= nt the complete set.

>which will it make necessary to= start defining a bunch of axioms/parameters.

>Coq certainly is the r= ight tool for such a venture, however, I recently cloned

'>pvslib= ' which uses SRI's PVS and I was surprised how close it is

>(= syntactically) to SPAD. i guess it would be my second choice.

>

&g= t;http://pvs.csl.sri.com

>https://github.com/nasa/pvslib/blob/master/interval_arith/interval.pvs<= /a>

Kurt,

I've been using Proo=
f General for COQ proof development.There are several in=
teresting points.

COQ has types as first-class objects. T=
his allows types like

nat to be effectively renamed into NNI=
. More likely, a COQ-based

NNI would extend COQ's nat typ=
e. It appears I can also do some

Spad-Category-like inheritan=
ce hierarchy. The net result would be

that "nearly nativ=
e" Spad code could be proven.

COQ also has a form of=
literate programming. COQ comments are

rendered as latex/pdf=
files. Latex commands can be embedded in the

comments. The net result i= s that a form of the final document is

directly executable.

--f403045d585e27ff1d054636bd7c--
From MAILER-DAEMON Wed Jan 25 03:18:15 2017
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1cWImV-0007bG-2l
for mharc-axiom-developer@gnu.org; Wed, 25 Jan 2017 03:18:15 -0500
Received: from eggs.gnu.org ([2001:4830:134:3::10]:53386)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from comments. The net result i= s that a form of the final document is

directly executable.

Proof General runs the coqtop interpreter as a separate process unde=
r

Emacs, similar to the Slime interface used for lisp. This a=
llows for the

forward and backward stepping in the file. Axio=
m has an undo command

so it seems possible to run the Axiom i=
nterpreter under Proof General.

That would allow interactive =
development of Spad code that could also

be proof-checked dur=
ing development.

This combination of factors could really=
change the way that Axiom code

is developed, leading to much=
higher code quality.

If I get time this semester I may t=
ry to develop the geometric algebra code

this way. It depends=
on how the class goes.

All things considers, you made a =
brilliant suggestion.

Tim

I was largely poking, tongue in cheek, at the earlier syll=
ogism:

--001a1148d1c41aafa10546e6dfc1--
From MAILER-DAEMON Wed Jan 25 10:39:17 2017
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1cWPfI-0003PC-Vq
for mharc-axiom-developer@gnu.org; Wed, 25 Jan 2017 10:39:17 -0500
Received: from eggs.gnu.org ([2001:4830:134:3::10]:60225)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from >>=C2=A0The po=
int is that Lisp has a formal logic basis and, as Spad is really

>> just a domain specific languag=
e implemented in Lisp then Spad shares

>> the formal logic basis.-- Gaby

On Thu, Jan 12, 2017 at 10:35 PM, Tim Daly <<=
a href=3D"mailto:axiomcas@gmail.com" target=3D"_blank">axiomcas@gmail.com> wrote:

He makes a distinction betwen invented and discovered langauge= s.shows= the logician's view versus the computer science view of various theori= es.> 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 "d= iscovered" language.

(begin quote of Wadler)

Every interesting logic has a= corresponding language feature:

Natural Deduction (Gentzen) <=3D= =3D> Typed Lambda Calculus (Church)

Type Schemes (Hindley) <=3D=3D= > ML Type System (Milner)

System F (Girard) <=3D=3D> Polymorphi= c Lambda Calculus (Reynolds)

Modal Logic (Lewis) <=3D=3D> Monads (= state, exceptions) (Kleisli, Moggi)

Classical-Intuitionistic Embedding (= Godel) <=3D=3D> Continuation Passing (Reynolds)

Linear Logic (Gira= rd) <=3D=3D> Session Types (Honda)

Languages which were "= discovered" (based on theory):

Lisp (McCarthy)

Iswim (Landin= )

Scheme (Steele and Sussman)

ML (Milner, Gordon, Wadsworth)

Haske= ll (Hudak, Hughes, Peyton Jones, Wadler)

O'Caml (Leroy)

Erlang (A= rmstrong, Virding, Williams)

Scala (Odersky)

F# (Syme)

Clojure (Hi= ckey)

Elm (Czaplicki)

At about minute 43 we hear:

"No= t 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 disco= vered; 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 "depend= ent types". It turns out that

when you extend into dependent types = you now get languages that

have "for all" and "there exis= ts" that corresponds to a feature

called "dependent types"= ;. So this means that you can encode very

sophisticated proofs, pretty m= uch 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 o= f these systems are based on a greater or lesser extent on

that idea:

Automath (de Bruijn)

Type Theory (Martin Lof)

Mizar (Trybulec)<= br>ML/LCF (Milner, Gordon, Wadsworth)

NuPrl (COnstable)

HOL (Gordon, = Melham)

Coq (Huet, Coquand)

Isabelle (Paulson)

Epigram (McBride, M= cKinna)

Agda (Norell)

(end quote)

Axiom is using Coq for i= ts proof platform because Axiom needs

dependent types (e.g. specifying m= atrix sizes by parameters).

In addition, Coq is capable of generatin= g a program from a

proof and the plan is to reshape the Spad solution t= o 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&= #39;s

NonNegativeInteger. Coq also has a 'Group' type which need= s

to be matched with the Axiom type. The idea is to find many

isomorp= hisms 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 likelythat a reasonable subset ca= n be proven (modulo the fact that thereare arguable differen= ces 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 L= isp code that are included.

I'm taking a course at Carnegie-Mell= on this semester using Lean

(a Coq offshoot) in order to try to make som= e working examples

of proving Spad code correct.On = Thu, Jan 12, 2017 at 10:14 PM, Gabriel Dos Reis <gdr@integrable= -solutions.net> wrote:T= here 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 <axiomcas@gmail.com> wrote:_________= _____________________the formal logic basis. =just a domain specific lang= uage implemented in Lisp then Spad sharesThe point is that Lisp has a for= mal logic basis and, as Spad is reallywhether your language is = discovered or invented".are "invented" with no formal basis = (e.g. C). As he says, "you can tell"discovered" based on fundamental logic principles (e= .g.Lisp) and others<= div>Types", a very entertaining talk, is= here:I'm making progress on proving Axiom correct both at the Spad = level andthe Lisp level. One interesting talk by Phillip Wadler = on "Propositions as

https://www.youtube.com/watch?v=3DIOiZatlZtGU

<= /div>He makes the interesting point late in the talk that some languages ar= e_________________

Axiom-developer mailing list

Axiom-devel= oper@nongnu.org

https://lists.nongnu.org/mailman/listi= nfo/axiom-developer

I got th=
e tongue-in-cheek aspect but Axiom's formal logic basis is important.

In the 1980s Expert Systems were going to take over the wo= rld. We tried to prove our version

Th=
ere was a complete mismatch with the rule-based expert systems technology.<=
br>

Because Axiom is so close to the math and Coq is so close=
to Axiom it seems there

is hope that this effort will make a=
lot more progress.

simplifies what is usually a hai= r-tearing struggle. Lean (a Microsoft/CMU) system is

the basis of a cou= rse I'm taking at CMU and it seems even more user-affectionate.

of a matrix. Since types =
can be user-defined we can create Axiom-specific types in Coq

that mirro= r the Category structure.Even sweeter is that the syntax is very close to S= pad.

that mirro= r the Category structure.Even sweeter is that the syntax is very close to S= pad.

For example, Spad

=C2=A0=C2=A0 gcd(x:N=
NI,y:NNI):NNI =3D=3D

=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 zero? x =
=3D> y

=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 gcd(y rem x, x)

<= br>

<= br>

and Coq

=C2=A0=C2=A0 Fixpoint gcd x y :=3D<=
br>

=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 match x with

=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0 | O =3D> y

=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0 | S x' =3D> gcd (y mod (S x')) (S 'x)

--001a114783ac75aedf0546ed0821--

where S is the Peano Successor function. Coq can prove this direct=
ly and

automatically infer that the type signature is

=C2=A0 gcd(x:nat,y:nat):nat

Coq pr=
oofs are now integrated into the build. The next commit will likely include=
complete

automation of the proof, calling Coq during the bui=
ld process with GCD as the first case.

Once that happens =
the game seems to be creating the Axiom type tower in Coq.

Ax=
iom's NNI becomes Coq's 'nat' type. This enables writing Ax=
iom types directly

in Coq proofs.

The ideal=
case would be to modify Axiom's compiler to accept the Coq/ML syntax

but that's a large effort.

Another, more=
likely effort, would be to implement Coq's trusted kernel in Axiom.

That would permit the compiler and interpreter to prove running=
code.

It is time to formalize computational mathematics =
and put computer algebra on

a firm mathematical basis. The te=
chnolgy is here (although the funding is not).

On Wed, Jan 25,=
2017 at 3:18 AM, Gabriel Dos Reis <gdr@integrable-solutions.ne=
t> wrote:

= I was largely poking, tongue in cheek, at the earlier syllogism:>>=C2=A0The po= int is that Lisp has a formal logic basis and, as Spad is really>> just a domain specific languag= e implemented in Lisp then Spad shares>> the formal logic basis.-- Gaby On Thu, Jan 12, 2017 at 10:35 PM, Ti= m Daly <axiomcas@gmail.com> wrote:=He mak= es a distinction betwen invented and discovered langauges.>= ; There were implementations of C in Lisp. So C shares that formal logic ba= sis, or that it was discovered?According to Wadle= r, C is an "invented" language, not a "discovered" lang= uage.shows the logician's= view versus the computer science view of various theories.

(beg= in quote of Wadler)

Every interesting logic has a corresponding lang= uage feature:

Natural Deduction (Gentzen) <=3D=3D> Typed Lambd= a Calculus (Church)

Type Schemes (Hindley) <=3D=3D> ML Type System= (Milner)

System F (Girard) <=3D=3D> Polymorphic Lambda Calculus (= Reynolds)

Modal Logic (Lewis) <=3D=3D> Monads (state, exceptions) = (Kleisli, Moggi)

Classical-Intuitionistic Embedding (Godel) <=3D=3D&g= t; Continuation Passing (Reynolds)

Linear Logic (Girard) <=3D=3D> = Session Types (Honda)

Languages which were "discovered" (b= ased 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 (Czapl= icki)

At about minute 43 we hear:

"Not all of these lang= uages 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 &qu= ot;invented". Looking at them

you can tell they are invented. So th= is is my invitation to you

to work in languages that are "discovere= d".

Somebody asked before about "dependent types". It= turns out that

when you extend into dependent types you now get languag= es that

have "for all" and "there exists" that corre= sponds to a feature

called "dependent types". So this means th= at 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 chec= k 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 (Hue= t, Coquand)

Isabelle (Paulson)

Epigram (McBride, McKinna)

Agda (No= rell)

(end quote)

Axiom is using Coq for its proof platform b= ecause Axiom needs

dependent types (e.g. specifying matrix sizes by para= meters).

In addition, Coq is capable of generating a program from a =

proof and the plan is to reshape the Spad solution to more

closely m= irror the proof-generated code. Also, of course, we needto r= emove any errors in the Spad code found during proofs.

It= seems there must be an isomorphism between Coq and Spad.

At the mom= ent it seems that Coq's 'nat' matches Axiom's

NonNegativ= eInteger. 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 i= t seems likelythat a reasonable subset can be proven (modulo= the fact that thereare arguable differences from the abstra= ct algebra type hierarchy).

Currently Coq is run during t= he 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 i= ncluded.

I'm taking a course at Carnegie-Mellon this semester us= ing Lean

(a Coq offshoot) in order to try to make some working examples<= br>of proving Spad code correct.= On Thu, Jan 12, 2017 at 10:14 PM, Gabriel Dos Reis <gdr@integra= ble-solutions.net> wrote:There were implementations of C in Lisp. So C shares that formal logic ba= sis, or that it was discovered?On Wed, Jan 11, 2017 at 8:17 PM, Tim Daly <axiomc= as@gmail.com> wrote:______________________________ the formal logic basis.just a domain specific language implemented in Lisp the= n Spad sharesThe point is that Lisp has a formal logic basis and, as Spad= is reallywhether your language is discovered or invented"= ."discovered= " based on fundamental logic principles (e.g.Lisp) and othersHe makes the interestin= g point late in the talk that some languages areTypes", a very entertaining talk, is here:I'm making pro= gress on proving Axiom correct both at the Spad level andthe Lis= p level. One interesting talk by Phillip Wadler on "Propositions as

https://www.yout= ube.com/watch?v=3DIOiZatlZtGU

are "invented" with no formal basis (e.g. C). As he says, "= you can tell_________________

Axiom-developer mailing list

Axiom-devel= oper@nongnu.org

https://lists.nongnu.org/mailman/listi= nfo/axiom-developer