Como chamar o Coq de assistente de prova de um software externo? Coq tem alguma API? A interface da linha de comandos Coq é rica o suficiente para passar argumentos no arquivo e receber resposta no arquivo? Estou interessado em pontes Java ou C ++.

Esta é uma pergunta legítima. Coq não é o software comercial usual do qual se pode esperar a API amigável para desenvolvedores. Eu tinha uma pergunta semelhante sobre Isabelle / HOL e era uma pergunta legítima com resposta não trivial.