The Coq mailing list

[David MENTRÉ <dmentre AT linux-france.org>]

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