日本でのTSMCの第2工場建設の遅れは交通渋滞のせいだとCEOが指摘、今後5年間でアリゾナ州に1000億ドルを投資する計画を再確認 - GIGAZINE
https://gigazine.net/news/20250604-tsmc-japan-delay-on-traffic/

[B! 知識] 堅揚げポテトの袋はマジックミラーになっている　内側からだけ向こうが見える。この性質を活用したい
https://b.hatena.ne.jp/entry/s/dailyportalz.jp/kiji/kataage-poteto-magic-mirror

アルミ蒸着フィルムがマジックミラーになるのって一般常識の範囲じゃないの・・・？＞＜

SBCでやるなら「FDDでも音楽記録メディアだよ！」になるだろうけど、Windowsとかでやろうとすると全部キャッシュされちゃって全く意味なさそう＞＜；

IoTなSBCにUSB-FDDとmp3デコーダチップを組み合わせたら、FDDからジコジコ音を出しながらmp3を読みつつ音楽再生できる音楽プレイヤーを作れるのかも・・・？＞＜

この記事読んでて思いついたけど、よく考えたら2HDのFDDの転送速度ってmp3のビットレートよりは速い（？）ということは、メディアがFDDな音楽プレイヤーって21世紀のテクノロジーで作れる・・・？＞＜；

【特集】PC-9800シリーズ風の現代PCを作ってみよう！～5インチFDDは動くのかも試してみた - PC Watch
https://pc.watch.impress.co.jp/docs/topic/feature/2019142.html

元オレアイダの操業工場で現在はハインツ所有のオレゴン州オンタリオの巨大冷凍食品工場もENERGY STARなので、おはようポテトもたぶん地球にやさしい・・・？＞＜

つまりマックフライポテトは地球にやさしい？＞＜（？）

Frozen Fried Potato Processingのところを見たら、マックフライポテトの工場（会社としてはシンプロットとかラムウェストンとか）が、わりとENERGY STARになってる＞＜

ENERGY STARな建物の数がカリフォルニアはテキサスの倍くらいあるの、すごくカリフォルニア＞＜（？）

建物のリストもあった＞＜
Registry of Certified Buildings and Plants | ENERGY STAR
https://www.energystar.gov/buildings/certified_buildings_and_plants

Commercial Buildings | ENERGY STAR
https://www.energystar.gov/buildings

建物に対しても、ENERGY STARあったのか＞＜；

FAQ お問い合わせ | 国際エネルギースタープログラム
https://www.energystar.go.jp/faq.html
"...さらに米国では、家電などの機器だけでなく、家屋・ビル等も対象に含まれており、販売員育成や購入資金補助など幅広い分野に対して実施されています。"

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

それは完全にそうだけど、ハードウェアに役割を与えるのがソフトウェアなわけだし・・・＞＜

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

セキュリティ的にあれかもだけど、学生のPCでも動かしたら、さすがに「サーバーって実はネットワークで繋がった計算機上で動くソフトウェアであって、俗に「サーバー」と言ってるのはそれを動かしてる計算機をそう呼んでるだけ」って理解できそうな気が＞＜
とにかく「ハードウェアじゃないんだ！　ソフトウェアなんだ！」だけを強調する感じで＞＜
(学生が「なんだこいつ」って思われるようになるかもだけど、間違ってはないし＞＜；)

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

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

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

もしかして、20世紀までに日本で普及した野菜で、「菜」がつく作物って全部が学術的な種としてはブラッシカ・ラパなのかな？＞＜
と思ってGeminiに聞いたら、「少なくともセイヨウアブラナ(Brassica napus)と、カラシナとタカナ(Brassica juncea)が例外としてあるかも」って教えてくれた＞＜

白菜も白菜も(？)、他の色々なhoge菜のわりと多くも、結局はブラッシカ・ラパ＞＜

ブラッシカ・ラパ - Wikipedia https://ja.wikipedia.org/wiki/%E3%83%96%E3%83%A9%E3%83%83%E3%82%B7%E3%82%AB%E3%83%BB%E3%83%A9%E3%83%91

どう違うか知らなかったのでググったけど、
結球する品種の白菜が「ハクサイ」で、結球しない品種の白菜が「シロナ」らしい・・・？＞＜

Geminiとこれを土台に議論したけど、Geminiは「形式検証って学習曲線がつらいかし、やっぱミッションクリティカル向けでは？」って反論してきて、
それに「むしろミッションクリティカルな環境以外ではオプショナルな導入で十分で『書きたい人が必要な部分にのみ』ってスタイルで良さそうだし、なにより形式検証によるエラーメッセージは初学者に対して優しいヒントになるんでは？＞＜」ってなって、
Geminiが「たしかにそういう発想でのオプショナルな導入であればかなり有用だし、初学者のアシストとしての形式検証環境ってコンセプトは新しいかも！」(意訳)
ってなった＞＜(実際はもっと長い議論です)

なんで、AdaでしかSPARKというか、契約プログラミングを土台にした形式検証プログラミングが全く流行らないんだろう・・・＞＜
C#とか構文的にも静的検査の環境が充実してる点でも向いてるだろうし、Rustとかの安全を売りにしてる環境向けにもあってよさそうなのに＞＜
10年前とかのプログラマが使うPCでは、契約プログラミングの検査は遅かったけど、いま時のPCなら全然遅くないし、昔と違ってコード記述中にIDEがバックグラウンドで構文検査するのが当たり前になりつつあるわけだから、静的検査の時間によるストレスもほぼ無いだろうし・・・＞＜

(Adaの)SPARKって、SPARK 1990とSPARK 2014で、目的は同じでもかなり違うのか・・・＞＜
SPARK 1990ではジェネリックプログラミングも明確に禁止してたのか＞＜

自身より圧倒的に開発がアクティブで現役のソフトウェアとの通信機能を削除って酷い＞＜；

SPARK—an annotated Ada subset for safety-critical programming | Proceedings of the conference on TRI-ADA '90
https://dl.acm.org/doi/10.1145/255471.255563
https://doi.org/10.1145/255471.255563