orange @[email protected]

鍵エアリプだけど、
だからこそ、アメリカの保守な人々って「開拓したのは我々だ！」って事を誇りというか自己正当化（？）に使ってるかも＞＜

後で自分でも読みたくなるかもだからログ共有＞＜
https://g.co/gemini/share/e369d0929c12

議論の本題かもしれない部分は、 "では、実際にその点について考察してみるとどうでしょうか？＞＜" 以降かも＞＜
最初の方は、Geminiが矛盾を見つけられるかをテストしたくてやってた部分だからあんまりおもしろくないかも＞＜

自分が議論したい内容の大半についての知識を持ってくれてる議論相手って人間ではめったに見つからないよ？＞＜；

全部読みたい人いる・・・？＞＜；

動的型付けって不要ではって話で、Geminiは「究極の安全性要件」("宇宙船の制御システムや医療機器など、絶対に失敗が許されないシステムにおいて")は、実行時にもバリデーションするじゃん」って話をしてきたけど、「実行時のバリデーションは動的型付けと関係ないだろ＞＜　むしろバリデーションの必要な範囲を実行前に検出するのも静的型検査だろ＞＜」って説明するのにAda/SPARKを使った＞＜

ちょうどさっきAda/SPARKで遊んだからこその結論かも＞＜；

Geminiさんのまとめ＞＜

簡単に言うと、人間がかかわらずとも完璧にプログラミングできるAIなるものが出来たとして、
完璧に動作するプログラムは、実行前に型がすべて決定されている（とりうる範囲が全て想定されている）物の事を言う（実行時にしかわからないものに関してバリデーションコードの漏れも無い状態）であるので、
未来の完璧なAIがコーディングした完璧なコードなるものは、完成の時点で既に型が決定しているので、
つまりそれは、定義上、静的型付けである＞＜
みたいな感じで合意が得られたかも＞＜

Geminiの主張の矛盾を（部分的に言及せずに終わったのもあるけど）片っ端から指摘していったら、仮にAIがとても賢くなったとして、消えるのは定義上、動的型付け言語の方であろうという結論で合意できたかも＞＜；

ガチガチの議論好きの人間相手の議論みたいになってるけど、相手が人間の時と違って相手のごはん食べる時間とか寝る時間とか気にしなくていいの素晴らしい＞＜；

なんか、Geminiに最初普通に感想を聞く形でさっきの記事について聞いたら、全然矛盾を見つけられなくてオレンジの指摘でやっと見つけられるという残念なことになったので、「この点とこの点とこの点について、このような矛盾がないか検証してほしい」みたいに注目させるプロンプトで聞いたら、
矛盾は相変わらず見つけられなかったけどなんかものすごい議論モードでの返答になって、そこからバチバチの議論になって超おもしろい＞＜＞＜

o4-miniは、わりと矛盾を見抜いてた＞＜
https://chatgpt.com/share/68302e05-7da0-8004-8f09-037e3b7cfc66

4o版はこれ＞＜
https://chatgpt.com/share/68302e2d-17c8-8004-a6c6-6318f2183ae3

4oでも一発で矛盾を見抜きそうと思いきや見抜けなかった＞＜；
指摘したら「確かにそう」ってなったけど＞＜；

まつもとゆきひろさん「Programming Language for AI age」～RubyKaigi 2025 3日目キーノート | gihyo.jp
https://gihyo.jp/article/2025/05/rubykaigi-2025-keynote-report-day3

なんで、コミュニケーションでのエラーの話を、統合された認識（知識）内でのエラーの話に挿げ替えてるの？＞＜

"...AIが出力したコードを読んで人間が修正したり、人間が書いたコードをAIが手直ししたりなど、AIと人間が相互にやり取りする場合、一般的には静的型付け言語が使いやすいと言われています。..."
"...ただ、未来のことを考えた場合、本当に静的型付けは必要だろうか、とまつもとさんは問いました。人間はうっかり型を間違えることがありますが、賢い人間は型エラーを起こさないので、十分に賢いAIは静的型付けなどなくても型エラーを起こさない、と言います。"

最初の記事は「ブログ始めます」なので、現在アクティブな内容がある記事は、たったひとつ、MySQL 5.7のドキュメントを参照している記事のみって事かも？＞＜；

興味がある人はAda/SPARKを使ってみよう＞＜
公式パッケージマネージャはこれ＞＜
Alire -
https://alire.ada.dev/