「ホーア論理とホーアオートマトン 1/n」の続きです。文字の色の約束は前回と同じです。「ホーア論理とホーアオートマトン 1/n // 文字の色の約束」を確認してください。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mbf}[1]{\mathbf{#1}} \newcomman…

AIコーディングエージェントの登場により、“狭い意味でのコーディング”はAIに任せられるようになりました。しかし、次の作業はまだ人間がやったほうがよさそうです。 プログラムの仕様の記述 テストの設計・計画 人間が、プログラムの仕様を記述して、テスト…

最近の証明支援系／プログラミング言語では、通常の型システムの上位に宇宙システム（ソートシステムともいう）を備えたものがあります。2023年の記事「最近の型理論： 宇宙と世界、そして銀河」の冒頭を引用すると： Lean（最新版はLean 4）は強力な型シス…

古典論理では、命題「Pでない ならば Qでない」の対偶である「Q ならば P」は、もとの命題と同値であり意味は変わらないとされます。しかし、対偶命題がもとの命題と同値なことは日常直感と合わない、とも言われます。そのとき出される実例のひとつに「言わ…

Lean のコード生成に関しては、GitHub Copilot の補完AIやエージェントはほとんど役に立ちません（むしろ、邪魔しやがる）。コーディングAIの利用は現実的でないので諦めました。とはいえ、Lean の複雑な言語仕様や巨大な Mathlib ライブラリを理解・把握で…