固定された投稿
自己紹介下書き2＞＜
超多趣味で、興味がある分野は、
航空(※1)宇宙開発鉄道物流都市計画都市緑化自動車(※2)送電線 南の島の電柱 クレーン橋梁トンネルダム廃道酷道 土木と公共事業と地域問題 土砂災害電子計算機 ヒューマンセンタードデザイン 建築地理地域ネタ 世界のローカルフード マイナードリンク郷土史冷戦史 虐殺問題と国連の役割 人種差別問題セクシャルマイノリティ差別問題 東欧の民主化 報道とその役割 放送局用機器シンセサイザーポピュラー音楽制作背景史アメリカ文化 アメリカのトラック輸送 大規模農業大型農業機械垂直農業農産物の安全保障紛争鉱物問題
かも＞＜
(※1 ジャーマンウィングス事故で世界で最初に、管制との最後の交信内容を言い当てた＞＜)
(※2 免許は無い＞＜)
ワードサラダ並み感＞＜；
いつもは「フィクションでも設定通りにちゃんと作れ＞＜」とブチ切れるオレンジが「これはこれで素晴らしい＞＜」と思ってしまう映画だった＞＜
でも通しでちゃんと見る気は全くしない＞＜；
撮影予算がほんとになければ雰囲気が近いライセンスフリーの映像をつなげばいいし、どうせ観客はゆりかもめの線路と近未来リニアのCGなんて見分けがつかないし、カリフォルニアの駅に駆け付ける救急車にでっかくワシントンDC（District of Columbia）と書かれてる映像が大きく映っても気にしない＞＜
CGが足りなければ戦闘機のプラモを映せばいい＞＜
逆に言うと、お金がなくても映画を作るという意気込みとツッコミどころしかない映画・・・＞＜；
ブレット・エクスプレス 弾丸特急 - YouTube
https://www.youtube.com/watch?v=PPqedhX60So
youtube公式無料映画にあった、サメ映画の会社がサメ映画のクオリティで低予算で作った鉄道パニック映画、飛ばし飛ばし見たけど、ストーリーがどうとかどうでもよくて、映画は割り切ればお金なんてそんなになくても作れるんだという意気込みが素晴らしかった＞＜
Sep 3, 2026
Mississippi city police chief fired over alleged racial slurs in texts | CNN
https://edition.cnn.com/2026/09/03/us/mississippi-police-chief-fired-senatobia
Mississippi officer and interim police chief resign after officer’s fatal shooting of 1-year-old in car during pursuit | CNN
https://edition.cnn.com/2026/10/23/us/mississippi-kohen-wiley-fatal-shooting
これ↓の感想をClaudeに尋ねたら、なぜかいつもの堅苦しいClaudeじゃなくGeminiみたいになった＞＜
https://mstdn.nere9.help/@orange_in_space/117493704344034673
欠陥品かどうかは別として、ある程度の類似性と部分的な相違がある感じかも＞＜
MBTIじゃなくビッグファイブだけど、日本語版AQを整備した若林明雄先生（共著者はバロンコーエン！＞＜；）の論文でこういうのもある＞＜
Are autistic traits an independent personality dimension? A study of the Autism-Spectrum Quotient (AQ) and the NEO-PI-R - ScienceDirect
https://www.sciencedirect.com/science/article/abs/pii/S0191886906001437
・・・みたいな事を言い出す人はMBTIのようなテストでINTPになる率が高いと思うよ！＞＜；（？）
orange
さんがブースト
INTPはASDだ！人間として欠陥品だ！って言う論調がX(蔑称)に蔓延っていてウケる
"あまりに意味不明な思想が流れてき"た という趣旨の鍵投稿を見かけて何だろうと思って探して、これなのかなというものを見つけたけど、それこそ言葉の定義を全く無視しててまったく意味不明すぎた＞＜（？）
（"デコンパイル"の話題とは別です＞＜）
あと、MatzとDHHは先見の明が無さすぎると思う＞＜
(両者とも意訳するとAIが扱うプログラミング言語に静的型検査が不要である主旨の事を言ってる)
オレンジ自分で先見の明って言っていいと思う＞＜
LLMs are making formal software verification feasible at a much larger scale \ Anthropic https://www.anthropic.com/research/formal-verification
orange
さんがブースト
ちなみに、本家本元である(？)Ada/SPARK環境自体に関しては、LLMさん的には参考できるコードがほとんど無いので(だって、兵器やら原発やら宇宙機やらの機密がいっぱいな分野向けの言語だし)、学習がほとんど出来てなくて、基本的な構文に関してでさえもハルシネーションを起こしまくり＞＜；
なので、既にLLMが得意な言語で型がそれなりにしっかりしてる言語向けの形式検証環境を用意するのがよさそうだし、
つまり、C#版のSPARKという選択肢は有力ではないか？＞＜；
orange
さんがブースト
オレンジが「AIの時代こそ契約プログラミングと形式検証ツールの復権を！＞＜；」って言っても誰も見向きしないであろうから、
プログラミングパラダイム界隈の有名人(？)の誰かが「・・・もしかして、AIの時代こそ、契約プログラミングと形式検証によって計算リソースを削減できるんじゃね？」って気づいてほしい＞＜；
orange
さんがブースト
orange
さんがブースト
で、その返答のなかで興味深い部分が＞＜；(強調は『』に置き換え)
"LLMの役割の最適化:
LLMは、要件定義の解釈、高レベルな設計、全体構造の生成、自然言語に近いコメントの付与など、『創造性や柔軟性が求められるタスク』に集中し、『厳密な論理的整合性のチェックやバグ検出は形式検証ツールに任せる』という分業が可能になります。これにより、それぞれのツールの得意分野を活かし、全体の計算リソースを効率的に配分できます。"
orange
さんがブースト
ほぼそのままGeminiに聞いてみたけど、形式検証は決定論的な検証で、LLM論は確率論的な検証になるので、原理的に(？)決定論的な検証の方が計算量が少なくなる(？)ので、オレンジが言う通り、形式検証の静的検査が重いといってもLLMがコードを読む為の計算量よりは少ないので、LLMが形式検証環境を使うと計算量を大幅に削減できる可能性が高いかも(意訳) みたいな感じだった＞＜
orange
さんがブースト
契約プログラミングや形式検証の静的検査が遅い/重いのはGeminiさんが言う通りの弱点ではあるだろうけど、でも、『LLMがコードを読んで考える』よりは少ない計算量になりそうな気がするけどどうなんだろう？＞＜
orange
さんがブースト
つまり、AI支援型プログラミングの時代こそ、形式検証や契約プログラミングが優れてるかもしれないので、なんか10年くらい前にブームが終わってしまった(？)契約プログラミングを、今こそ復権させるべき！！！＞＜；
orange
さんがブースト
AdaのSPARKみたいな形式検証をプログラミング言語環境側に用意してあったら、ハルシネーションの大半にAIが自身で気づけるかもだし、形式検証とAIって相性どうだと思う？＞＜(意訳)って、Geminiさんに聞いてみたら、
「(形式検証で検出できる範囲において)単にハルシネーションに気づけるだけではなく、AIが形式検証エラーのメッセージを読むことで自律的に学習出来るので、SPARKみたいな形式検証とAIの組み合わせはすごくいいはず。でも、規模が大きいプロジェクトでは、AIが出力する契約プログラミングのコードが膨大になって、形式検証の実行に時間がかかってボトルネックになりそう」(意訳)
みたいに言われた＞＜
- ＠orange_in_space
2017年 4月に登録
