開発をシフトレフトせよ――形式仕様でAIと事前に合意する開発のすすめかた

AI への指示書は自然言語で書きます。 書いた本人には明確に見えますし、AI も分かったという顔をして実装を始めます。 その結果、できあがったものが思っていたものではないことがあります。 なぜなら、自然言語は解釈が揺れるからです。 私が開発している OSS の TAKT では、この揺れを実行前の対話で潰しています。 具体的には、アシスタントとタスクを詰めて合意した内容を、指示書にまとめてからエージェント群に渡すようにしています。 この指示書の受け入れ条件はこれまで Gherkin で書かせてきました。 v0.61.0 でここに形式仕様モードという設定を足しました。 有効にすると、指示書の要件を Quint と Alloy という記法でも表現するようになります。 形式手法は正しさが欲しい場面で昔から使われてきた道具です。 ただ実務で常用するには仕様を書いて維持するコストが高く、採用できないと

[auto_chan]

開発の左傾化！レッドシフト！

[yarumato]

“自由文で書かれた仕様書はぶれやすく、読みづらいものです。というか読みたくない。形式手法は正しさが欲しい場面で昔から使われてきた道具だが、実務で常用するには仕様を書くコストが高かった。今はAIがある。”

[toaruR]

だんだんコードになっていく(ノ∀`)

[simplememofast]

検証器を回さない以上、iff仕様が誤れば下流は忠実に誤りを答え合わせする。曖昧さを自然言語から形式記法へ移した形で、どこから総当たり検証に踏み込むかが次の論点だ

[mkusaka]

TAKTのformal_specでAIと事前合意し、Gherkinに加えQuint/Alloyで要件を曖昧さ除去する開発手法。

[moronbee]

"これまで先送りできていたことの一部が先送りできなくなったわけで、マインドチェンジが求められます。結果として、開発における意思決定はどんどん手前に寄っていく。"

[otihateten3510]

AIこういうの苦手そう

[hasiduki]

形式手法の時代きたー！！！！！！！！！

[fuji_haruka]

“Quint と Allo”

[nguyen-oi]

形式手法をAIに書かせる発想は面白いな。仕様の曖昧さを手前で潰すのは理にかなってる