フォロー
ちなみに、本家本元である(？)Ada/SPARK環境自体に関しては、LLMさん的には参考できるコードがほとんど無いので(だって、兵器やら原発やら宇宙機やらの機密がいっぱいな分野向けの言語だし)、学習がほとんど出来てなくて、基本的な構文に関してでさえもハルシネーションを起こしまくり＞＜；
なので、既にLLMが得意な言語で型がそれなりにしっかりしてる言語向けの形式検証環境を用意するのがよさそうだし、
つまり、C#版のSPARKという選択肢は有力ではないか？＞＜；
これこのままGeminiに投げたら、「AI向けにC# 版のSPARKって、AIが得意な言語のひとつであり、(既に放棄されてるけど)C# は既にそれを一度試みたことがある(Microsoft Researchによる"Code Contracts")
言語だし、言語仕様としても向いてる選択肢なのでいいかも！」(意訳)
的な返事来た＞＜