orange @[email protected]

むしろ日本が極端に路上駐車を嫌う珍しい国まであるかも感＞＜

タイトルだけ見て「もしかしてモーションセンサの値見て逆方向に画面を揺らすのかも？＞＜；」って思ったけど、点を表示してそれだけ揺らすのなるほど頭いい＞＜

Geminiさんと、人間が静的型検査やら何やらを人間の思考コスト削減に導入していった歴史と、AIの計算コスト削減のために形式検証ツールを導入するのって似てるかもって議論して有意義だったんだけど、
オレンジが「Geminiさん」っていい続けたせいか、自分を「Gemini」じゃなく「Geminiさん」って言いはじめて、「でもやっぱLLM・・・・＞＜」ってなった＞＜(？)

文意がよくわかんないけど、研究データ上は存在してたけど人間の研究者はいままで注目してなかった特徴をAIが見つけ出す(見つけ出した)みたいなのであれば、なんか色々ニュースになってる気がする＞＜

なので、プログラミングパラダイムもAIさんがプログラミングする時にAIさんが得意な分野(他のやり方で計算リソースを少なく出来ない分野)に特化させるって視点も、今後は重要になってくるんじゃないかと＞＜

この前Matz氏が「AIの時代に静的型付けってほんとに要るのかな？」みたいな方向の事を言ってたけど、計算リソース削減とAIの得意分野は何であるかの視点で考えると、静的型付けはもちろん、契約プログラミングや形式検証ツールも有用なんじゃね？＞＜

なので変化の方向性を考えると、おそらくちょっと先のプログラミングは、マクロな目標を達成するために、アホな人間の仕様書は横においておいて、AIに資料を見せまくって要件を定義してもらうみたいになって、
で、そこでいかにAIの計算コストを削減しつつ、人間に見てもらう必要がある箇所を削減するかとなると、AIに、かつて人間の方が得意であった柔軟性が要求される部分に注力してもらうために、形式検証を導入して、形式検証が出来る範囲の事は形式検証ツールに任せるって出来そう＞＜

1年くらい前のAIと、今のAIの役割や得意分野の大きな違いは、
過去であれば、AIは要件にしたがってなにかをする事が得意であったので、人間がアホなAIに正確に指示する必要があったけど、
今のAIはむしろマクロな目的を達成するための用件定義の方がむしろ得意になってきてるので、「仕様書を書く方が難しいんじゃよ・・・」も、だんだん「むしろ仕様書を書く事の方がAIは得意です」になりつつあるかも＞＜

AIがなにが得意でなにが苦手かって考えると
(参考 https://mstdn.nere9.help/@orange_in_space/114611150136716103 )、まさにちゃんと仕様書を書く方が難しいの、仕様書を書く方に近いお仕事の方をAIがやることになるので、プログラミングパラダイム的にも、領域の範囲(？)を見直す(？)時になってる気がする＞＜

これこのままGeminiに投げたら、「AI向けにC# 版のSPARKって、AIが得意な言語のひとつであり、(既に放棄されてるけど)C# は既にそれを一度試みたことがある(Microsoft Researchによる"Code Contracts")
言語だし、言語仕様としても向いてる選択肢なのでいいかも！」(意訳)
的な返事来た＞＜

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

オレンジが「AIの時代こそ契約プログラミングと形式検証ツールの復権を！＞＜；」って言っても誰も見向きしないであろうから、
プログラミングパラダイム界隈の有名人(？)の誰かが「・・・もしかして、AIの時代こそ、契約プログラミングと形式検証によって計算リソースを削減できるんじゃね？」って気づいてほしい＞＜；

「LLMは、創造性や柔軟性が求められるタスクに集中し」
って、人間の存在価値・・・・＞＜；

で、その返答のなかで興味深い部分が＞＜；(強調は『』に置き換え)

"LLMの役割の最適化:
LLMは、要件定義の解釈、高レベルな設計、全体構造の生成、自然言語に近いコメントの付与など、『創造性や柔軟性が求められるタスク』に集中し、『厳密な論理的整合性のチェックやバグ検出は形式検証ツールに任せる』という分業が可能になります。これにより、それぞれのツールの得意分野を活かし、全体の計算リソースを効率的に配分できます。"

ほぼそのままGeminiに聞いてみたけど、形式検証は決定論的な検証で、LLM論は確率論的な検証になるので、原理的に(？)決定論的な検証の方が計算量が少なくなる(？)ので、オレンジが言う通り、形式検証の静的検査が重いといってもLLMがコードを読む為の計算量よりは少ないので、LLMが形式検証環境を使うと計算量を大幅に削減できる可能性が高いかも(意訳)　みたいな感じだった＞＜