The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

For this, you probably want to have a look at MathScheme.

On Fri, May 23, 2014 at 8:21 PM, Daniel Schepler 
<dschepler AT gmail.com>
 wrote:
> 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".
>
> I don't know that much about how existing CASes are structured,
> though, so I don't know how much I could contribute to such a project.
>  We could hopefully leverage some of the existing open source CAS
> projects like Axiom and Maxima for ideas, though I've only really used
> Maxima myself, and that not very seriously.
> --
> Daniel Schepler
>
> On Fri, May 23, 2014 at 8:16 AM, Jonathan 
> <jonikelee AT gmail.com>
>  wrote:
>> I'd be interested in finding out if there are any funded open-source
>> projects to use Coq that are looking for help.  The open-source ones
>> couldn't hide how seriously they employ Coq.
>>
>> I might be headed in the direction of starting such a project myself - but
>> I'd certainly want to know about others first.
>>
>> -- Jonathan
>>
>>
>> On 05/23/2014 11:06 AM, Adam Chlipala wrote:
>>>
>>> I think the risk here is that some companies will hint at more serious Coq
>>> use than they actually employ in real product-oriented activity, as a 
>>> trick
>>> to pull in the best developers. ;)
>>>
>>> On 05/23/2014 11:01 AM, David MENTRE wrote:
>>>>
>>>> Le 23/05/2014 16:43, Adam Chlipala a écrit :
>>>>>
>>>>> And how is a random person meant to learn more about the details?
>>>>
>>>>
>>>> It is difficult. It is not usual habit for companies to talk about their
>>>> practices (and nowadays everything is "confidential" in a company).
>>>>
>>>>> If I
>>>>> spent a little time poking around their web sites, would I get a good
>>>>> sense?
>>>>
>>>>
>>>> Probably not, for above reasons.
>>>>
>>>> Most of the time I found those kind of information through direct
>>>> discussion or through a few lines in a slide.
>>>>
>>>> For Trusted Labs, you'll find some basic information by googling "trusted
>>>> labs coq" or "trusted logic coq". But probably not detailed enough for an
>>>> advanced user like you.
>>>>
>>>> Sincerely yours,
>>>> david
>>>>
>>>
>>