orange @[email protected]

AdaのSPARKみたいな形式検証をプログラミング言語環境側に用意してあったら、ハルシネーションの大半にAIが自身で気づけるかもだし、形式検証とAIって相性どうだと思う？＞＜(意訳)って、Geminiさんに聞いてみたら、
「(形式検証で検出できる範囲において)単にハルシネーションに気づけるだけではなく、AIが形式検証エラーのメッセージを読むことで自律的に学習出来るので、SPARKみたいな形式検証とAIの組み合わせはすごくいいはず。でも、規模が大きいプロジェクトでは、AIが出力する契約プログラミングのコードが膨大になって、形式検証の実行に時間がかかってボトルネックになりそう」(意訳)
みたいに言われた＞＜

コーディングエージェントの現状の整理とエンジニアの仕事の変化について https://azukiazusa.dev/blog/coding-agents-and-developers-work

いま話題の(？)これ読んでて思いついたけど、
AIの自立型プログラミングでのハルシネーション抑制に、AdaのSPARKのように『契約プログラミングの記述を使った形式検証環境』をプログラミング言語側に用意したら、『形式検証で検出できる範囲のハルシネーションによる誤り(＝実行時にエラーを起こして停止するような誤りの大半)』は、AIがSPARKみたいなのを動かして形式検証エラーのエラーメッセージを読む事で自分で自分のハルシネーションに気づけるようになると思うんだけどどうだろう？＞＜

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

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

「RSA-260」ついに解けた　Xに“130ケタの数字”投稿、世界が注目　マスク氏「文字数増やしてよかった」（ITmedia NEWS） - Yahoo!ニュース
https://news.yahoo.co.jp/articles/d494e0bfa5872669dffe3a7b293e766bb898ee24

これからふと思って色々試したりして知ったけど、
RSAの計算が成り立つ最小限である4bitのRSAって作ろうとすると、必ず秘密鍵と公開鍵が同じになって「暗号とは？＞＜；」となる珍妙なものができる？＞＜；

[B! Windows] 今後のWindows 11からは「.NET Framework 3.5」が同梱されなくなる！？2010年前後に制作されたアプリケーションが動作しなくなる可能性あり | Game*Spark - 国内・海外ゲーム情報サイト https://b.hatena.ne.jp/entry/s/www.gamespark.jp/article/2025/10/14/158345.html

その頃に作ってたアプリなんだったのかすらもう覚えてないけど、
もしオレンジが当時 .NET Framework 3.5で作って配ってたアプリを使ってて、Windows 11でも使いたいのに動かなくて困ってる人が万が一居たら、ソース紛失してても出来る限りそれと全く同じ機能のものを作るので言ってね＞＜
(オレンジは配ったソフトウェアのサポートは無期限ってポリシー＞＜)

PHPでも、ちゃんと移行期間が用意されていて、将来使えなくなる命令や呼び出し方をすると、Deprecatedの警告出してくれたりするんだけど、日頃から全く更新をしていないと、移行期間を経ずにいきなり新しい書き方に対応しないといけない。

PHPどうこうじゃなく日頃から不断のメンテが必要なのであって「動かなくなるの怖いからバージョン固定して塩漬けっ☆ミ」とかやってる場合じゃないんだよという顔してる。

ただ、番号付け直しすると全部前に詰められちゃうんだけど。