Coq によるソフトウェアの品質保証について

Question

実現したいこと

Coq を用いてプログラムの単体テスト自動化をしたい

前提

C#、Python、Typescript で開発をしている

質問内容

Coq を用いればプログラムの単体テストの自動化をできることを知ったのですが、Coq で検証ができるプログラムは Coq または OCaml で記述されたプログラムに限られるのでしょうか？

Comments

[sasaki0628]

「やってほしいこと」を質問しているのではなく、すでに作られたプログラムをCoqで検証をするのは不可能なのか、Coqで検証ができるように最初からOCamlで開発をする必要があるのか、という質問をしています。

Answer 1

Coq で記述して正当性を確かめたあと OCaml や Haskell に変換をするのが主流だということがわかりました。