The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

Some interesting pointers, thanks.  As I indicated, I wasn't all that
serious about the idea as I'd have to do it in my spare time, and I
was fairly certain that wouldn't get me very far starting from
scratch.  I'm glad to see there are some serious projects out there
along these lines, though.
-- 
Daniel Schepler

On Fri, May 23, 2014 at 12:22 PM, Catalin Hritcu
<catalin.hritcu AT gmail.com>
 wrote:
> 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
>>