The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

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
>>>
>>
>