Re: [EXTERNAL] Re: Axiom's Sane redesign musings

Tim,

This all seems to be about the lisp layer, obviously thats what 
interests you.

It seems to me that if SPAD code is complicated and not aligned to type 
theory then, when SPAD is complied to Lisp, the List code will be 
complicated and hard to work with. Your previous remarks, about not 
seeing the whole elephant, suggest to me that you are drowning in 
complexity. Most languages, in their lifetime, acquire some messiness 
that needs to be cleared out occasionally.

Don't you think its time for SPAD 2.0 ?

Martin

On 30/06/2019 02:17, Tim Daly wrote:
> One major Sane design decision is the use of CLOS,
> the Common Lisp Object System.
> 
> First, since each CLOS object is a type it is possible to
> create strong types everywhere. This helps with the ultimate
> need to typecheck the compiler and the generated code.
> 
> Second, CLOS is an integral part of common lisp. One of
> the Sane design goals is to make it possible to use Axiom's
> domains in ordinary lisp programs. Since Axiom is nothing
> more than a domain specific language on common lisp it
> makes sense to construct it so users can freely intermix
> polynomials with non-algebraic code.
> 
> Third, CLOS is designed for large program development,
> hiding most of the implementation details and exposing
> a well-defined API. This will make future maintenance and
> documentation of Axiom easier, contributing to its longer
> intended life.
> 
> So for a traditional Axiom user nothing seems to have
> changed. But for future users it will be easy to compute
> an integral in the middle of regular programs.
> 
> Tim
> 
> On 6/27/19, Tim Daly <[email protected]> wrote:
>> Another thought....
>>
>> There has been a "step change" in computer science in the last few years.
>>
>> Guy Steele did a survey of the use of logic notation in conference papers.
>> More than 50% of the papers in some conferences use logic notation
>> (from one of the many logics).
>>
>> CMU teaches their CS courses all based on and requiring the use of
>> logic and the associated notation. My college mathematics covered
>> the use of truth tables. The graduate course covered the use of
>> Karnaugh maps.
>>
>> Reading current papers, I have found several papers with multiple
>> pages containing nothing but "judgements", pages of greek notation.
>> If you think Axiom's learning curve is steep, you should look at
>> Homotopy Type Theory (HoTT).
>>
>> I taught a compiler course at Vassar in the previous century but
>> the Dragon book didn't cover CIC in any detail and I would not
>> have understood it if it did.
>>
>> The original Axiom software predates most of the published logic
>> papers, at least as they applied to software. Haskell Curry wrote
>> from the logic side in 1934 and William Howard published in 1969
>> but I only heard of the Curry-Howard correspondence in 1998.
>>
>> Writing a compiler these days requires the use of this approach.
>> In all, that's a good thing as it makes it clear how to handle types
>> and how to construct software that is marginally more correct.
>>
>> The new Sane compiler is building on these logic foundations,
>> based on the Calculus of Inductive Construction and Dependent
>> Type theory. The compiler itself is strongly typed as is the
>> language it supports.
>>
>> Since dependent types are not decidable there will always be
>> heuristics at runtime to try to disambiguate types, only now we
>> will have to write the code in greek :-)
>>
>> Tim

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