orange @[email protected]

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の方が大半の人にとって安全に書きやすい」みたいな事を言ってて「そうなの？＞＜；」ってなったけど、実際に弄ってみると、なるほど数学の証明かも＞＜；

SPARKに怒られてるのはこういうコード＞＜

Geminiさんに（ハルシネーションで間違った指示もありつつも）いろいろ教えてもらいながら、やってみたら、AdaのSPARK使えた！＞＜

今日のトリビア＞＜

ドイツの堆肥ぶん撒きマシンのメーカー、BRIRIの社名の由来は、（たぶん）経営者2代のファミリーネームが由来で、ブリンク＋リーペンハウゼンで、ブリリ＞＜

つまり、ブリンクさんの会社をリーペンハウゼンさんが継いだから、ブリンク＋リーペンハウゼンで、ブリリという日本人的には奇跡的な会社名になったっぽい＞＜；

ドイツの堆肥ぶん撒きマシンメーカーのBRIRI、
社名の由来を調べたけど、
元々はBrink家がやってた村の鍛冶屋さんで、1918年にFranz Brinkさん（フランツ・ブリンク）が継いで、さらに1954年にAlfons Riepenhausenさん（アルフォンス・リーペンハウゼン）が継いでBRIRIになったらしい・・・＞＜

[pdf] https://briri.de/wp-content/uploads/2024/12/transporttechnikDE2023-web.pdf

ニュース記事のタイトルでコンゴ民主共和国を『コンゴ』って書くの、アメリカに関するニュースのタイトルで、事象から区別がつかない場面で『ワシントン』って書くのと同じくらいダメだと思う＞＜；
（例えば「ワシントンで銃撃事件」ってタイトルだと、ワシントン州の話かD.C.方の話かわからん＞＜）

[B! アメリカ] トランプ氏主張の「白人迫害」映像、コンゴで撮影の無関係動画と判明
https://b.hatena.ne.jp/entry/s/jp.reuters.com/world/us/KV5K5GWVXBIQHK7OPI72MIUTJ4-2025-05-22/

「トランプ支持者って本当にコンゴと南アフリカの区別ついていないと思う」という趣旨のブコメがあるけど、日本人の大半も『コンゴ共和国（コンゴ、西にある小さいの）』と『コンゴ民主共和国（旧ザイール、東にあるでかいの）』の区別がつかないと思う＞＜；
この記事の『コンゴ』は、『コンゴ民主共和国（旧ザイール）』の方＞＜

ドイツ南部(南端エリア？)では、パスタのようなものをお菓子としても食べるっぽい！？＞＜
という事は、その地域の人々であれば日本のイチゴショートケーキ焼きそば(と称する麺状のお菓子)も理解される？＞＜

シュペッツレ - Wikipedia https://ja.wikipedia.org/wiki/%E3%82%B7%E3%83%A5%E3%83%9A%E3%83%83%E3%83%84%E3%83%AC

こんなおもしろい社名なのに、ググってもオレンジ以前にこの事を言及してる日本人がみあたらないの不思議＞＜；

インタビュー動画とかも見る限り、発音は「ブリリ」であってるっぽい？＞＜；

ドイツの堆肥ぶん撒きマシンメーカー、BRIRIの公式動画＞＜

BRIRI Die Poleposition der organischen Duengung https://www.youtube.com/watch?v=UDVdcLEyCj8

発音も聞けるけど「ブリリ」なのか「ブイリ」(？)なのかいまいち聞き取れない＞＜；