The Coq mailing list

[Catalin Hritcu <catalin.hritcu AT gmail.com>]

CoqEAL - The Coq Effective Algebra Library
http://www.maximedenes.fr/content/coqeal-coq-effective-algebra-library

On Fri, May 23, 2014 at 9:08 PM, David MENTRÉ 
<dmentre AT linux-france.org>
 wrote:
> Hello,
>
> 2014-05-23 20:21, Daniel Schepler:
>>
>> I've toyed with the idea of starting a project for a formally verified
>> Computer Algebra System.  One of my high-level design goals would be
>> to make all the functionality accessible directly through Coq, in
>> addition to the more conventional "command line" type interface, in
>> order to be able to extract "proofs by reflection".
>
>
> Isn't it what is doing Georges Gonthier and his team in Coq/SSReflect?
>
>> I don't know that much about how existing CASes are structured,
>
>
> For Axiom: a Common Lisp base system, then two layers of home made
> languages, then a ton of libraries with cyclic dependencies (you need Axiom
> to compile Axiom, like a compiler).
>
> But Tim Daly (lead Axiom developer) would probably tell you that the real
> difficulty is not to build the core CAS, it is to build the ton of libraries
> needed for real mathematical work. Axiom was developed over more than 30
> years at IBM.
>
> If you really want to continue this path, you should probably contact Tim
> Daly. He was interested in formally verified CAS.
>
> Best regards,
> david
>