The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

sorry, forgot to include list :-)

On Tue, Jul 30, 2013 at 4:39 PM, Kristopher Micinski
<krismicinski AT gmail.com>
 wrote:
> What tactics might you want?  I'm not familiar with the full power of
> Matlab or Octave, but I assume it would aid certain decision
> procedures (or allow you to code them up).  As Adam points out you'll
> also need a way to generate a proof certificate from your
> Matlab/Octave code, if you want to minimize the trusted computing base
> to the Coq kernel.  (I'm uncertain if anyone's written up a generic
> way to transmit and handle proof certificates between processes,
> however, that seems like an interesting idea..)
>
> Kris
>
>
> On Tue, Jul 30, 2013 at 2:00 PM,  
> <pfirodmoten AT gmail.com>
>  wrote:
>> Is it possible to create tactics in Coq that use Matlab or Octave?