こんな感じ＞＜
簡単に言うと、人間がかかわらずとも完璧にプログラミングできるAIなるものが出来たとして、
完璧に動作するプログラムは、実行前に型がすべて決定されている（とりうる範囲が全て想定されている）物の事を言う（実行時にしかわからないものに関してバリデーションコードの漏れも無い状態）であるので、
未来の完璧なAIがコーディングした完璧なコードなるものは、完成の時点で既に型が決定しているので、
つまりそれは、定義上、静的型付けである＞＜
みたいな感じで合意が得られたかも＞＜
Geminiの主張の矛盾を（部分的に言及せずに終わったのもあるけど）片っ端から指摘していったら、仮にAIがとても賢くなったとして、消えるのは定義上、動的型付け言語の方であろうという結論で合意できたかも＞＜；
ガチガチの議論好きの人間相手の議論みたいになってるけど、相手が人間の時と違って相手のごはん食べる時間とか寝る時間とか気にしなくていいの素晴らしい＞＜；
なんか、Geminiに最初普通に感想を聞く形でさっきの記事について聞いたら、全然矛盾を見つけられなくてオレンジの指摘でやっと見つけられるという残念なことになったので、「この点とこの点とこの点について、このような矛盾がないか検証してほしい」みたいに注目させるプロンプトで聞いたら、
矛盾は相変わらず見つけられなかったけどなんかものすごい議論モードでの返答になって、そこからバチバチの議論になって超おもしろい＞＜＞＜
まつもとゆきひろさん「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のドキュメントを参照している記事のみって事かも？＞＜；
orange
さんがブースト
あれ、3記事目だったんだ。前の記事で参照しているMySQLのドキュメントがバージョン5.7で「あー、ね」となった。
https://honda-techblog.hatenablog.com/
興味がある人はAda/SPARKを使ってみよう＞＜
公式パッケージマネージャはこれ＞＜
Alire -
https://alire.ada.dev/
なんというか、静的型検査の超進化版っぽさ＞＜
C# にSPARKほしい＞＜；
契約プログラミングが使えることがすごいわけじゃなくて、『契約プログラミングで安全を数学的に証明できるようにコーディングしないと警告が出る環境』だから失敗したら人が死ぬ分野でも使える環境って、なるほどだし、
SPARKが無かった頃のAdaによる実装で起きたAriane 5の最初の打ち上げでの打ち上げ失敗（クラスターミッション）みたいなのを防げる技術なのか＞＜
クラスターミッション - Wikipedia
https://ja.wikipedia.org/wiki/%E3%82%AF%E3%83%A9%E3%82%B9%E3%82%BF%E3%83%BC%E3%83%9F%E3%83%83%E3%82%B7%E3%83%A7%E3%83%B3
素のAdaだとそのままビルドできちゃう整数を2倍にするだけの関数も、SPARK環境だとヘッダでの宣言のほうにこういう風に前提条件を書かないと警告が出ちゃう＞＜
なるほど数学好きな人向けの環境・・・・＞＜（数学好きじゃない＞＜；）
Ada/SPARK環境、なんか単に契約プログラミングで自動的に安全にしてくれるような環境を想像してたけど、
どっちかというと、数学的に証明不可能になってる数学的に曖昧な記述の個所を検査機(gnatprobe)が見つけ出して、契約プログラミングの記述で条件を指定して数学の証明の文脈で安全性を確保できるコードに書き換えさせる環境みたいな感じなのか・・・＞＜
前にChatGPTと「Ada/SPARKの方がRustよりも安全なんじゃないの？＞＜；」って議論した時に
GPTさんが「数学的な証明が好きな人はSPARKの方が向いてるけど、そこらのプログラマが皆、厳密な数学の証明の考え方で物事を考えてるわけではないので、Rustの方が大半の人にとって安全に書きやすい」みたいな事を言ってて「そうなの？＞＜；」ってなったけど、実際に弄ってみると、なるほど数学の証明かも＞＜；
今日のトリビア＞＜
ドイツの堆肥ぶん撒きマシンのメーカー、BRIRIの社名の由来は、（たぶん）経営者2代のファミリーネームが由来で、ブリンク＋リーペンハウゼンで、ブリリ＞＜
- ＠orange_in_space
2017年 4月に登録
