13:20:53

VS2022 17.14.7から17.14.8へのアップデート、なんでセキュリティ修正だけなのに2.74GBも・・・><

09:32:10
2025-05-23 19:44:55 orangeの投稿 orange_in_space@mstdn.nere9.help

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

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

09:31:57
2025-05-23 19:30:08 orangeの投稿 orange_in_space@mstdn.nere9.help

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

09:30:38
2025-05-23 19:23:07 orangeの投稿 orange_in_space@mstdn.nere9.help

Geminiさんのまとめ><

09:30:32
2025-05-23 19:19:47 orangeの投稿 orange_in_space@mstdn.nere9.help
こんな感じ><

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

09:30:10
2025-05-23 18:48:09 orangeの投稿 orange_in_space@mstdn.nere9.help

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

09:29:19
2025-05-23 16:53:39 orangeの投稿 orange_in_space@mstdn.nere9.help

まつもとゆきひろさん「Programming Language for AI age」~RubyKaigi 2025 3日目キーノート | gihyo.jp
gihyo.jp/article/2025/05/rubyk

なんで、コミュニケーションでのエラーの話を、統合された認識(知識)内でのエラーの話に挿げ替えてるの?><

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

まつもとゆきひろさん「Programming Language for AI age」~RubyKaigi 2025 3日目キーノート | gihyo.jp
09:23:10

決定論的に検証できるツールがあるからこそ、ゆるふわである人間が安全にプログラミングできるというのは、確率論的でゆるふわなLLMによるプログラミングでも同じで、型検査や形式検証を行えばLLMさんも自分が書いたコードの誤り(矛盾)に気付けるかも><

09:19:30

LLM側が決定論的じゃない問題って、プログラミング言語側が決定論的であるならば結果的に全く問題ないとオレンジは考えていて、
だからこそ、LLMを活用したプログラミングにこそ、静的型付けや形式検証(や契約プログラミング)が重要になってくるかもって気がしてる><

09:15:57
2025-07-14 09:13:46 ぽな (C.Ponapalt)の投稿 ponapalt@ukadon.shillest.net

プログラミングみたいな比較的決定論寄りの話だけでなくて、もっとふわっとした創作がらみでも、間に確率的なレイヤーが挟まると刃のキレが悪くなる的な感覚があってなあ…

09:15:49
2025-07-14 09:10:07 Satoshi Kojima (小嶋智)の投稿 skoji@sandbox.skoji.jp

このアカウントは、notestockで公開設定になっていません。

09:15:39
2025-07-14 09:08:08 Satoshi Kojima (小嶋智)の投稿 skoji@sandbox.skoji.jp

このアカウントは、notestockで公開設定になっていません。

09:15:35
2025-07-14 08:36:03 zundaの投稿 zundan@mastodon.zunda.ninja

LLMは面倒そうだしそのうち料金も高くなりそうだし電気も無駄遣いしてそうな気がするので触りません

09:15:31
2025-07-14 08:33:58 Satoshi Kojima (小嶋智)の投稿 skoji@sandbox.skoji.jp

このアカウントは、notestockで公開設定になっていません。

09:13:20

T4?><

09:13:11
2025-07-14 07:53:00 mzpの投稿 mzp@mstdn.nere9.help

カリフォルニアっぽい展示車

09:03:27

Windows XPの丘の近所だ><

09:03:10
2025-07-14 07:10:35 nezuko_2000の投稿 nezuko_2000@mstdn.nere9.help

ソノマ・レースウェイだ!

09:03:06
2025-07-14 06:03:48 mzpの投稿 mzp@mstdn.nere9.help

レース見にきた