LEANってどう使うの?
1132人目の素数さん
2025/12/31(水) 16:13:15.85ID:/bo6pYIm 教えて
2025/12/31(水) 17:09:02.72ID:kkckyp2e
リーン
3132人目の素数さん
2025/12/31(水) 18:00:56.81ID:bzes8faD タクティクが何してんのか全くわからん
4132人目の素数さん
2025/12/31(水) 19:24:53.08ID:Uu7+V9TL チーン
2025/12/31(水) 21:20:11.75ID:YyQrmwcP
2026/01/01(木) 15:40:39.23ID:6l379VoT
💩
7unko
2026/01/02(金) 07:10:22.67ID:liQzTJv5 💩をcleanしよう。
8132人目の素数さん
2026/02/11(水) 17:41:04.92ID:U3QT3rBs9132人目の素数さん
2026/02/11(水) 19:37:31.19ID:U3QT3rBs2026/02/11(水) 22:04:49.72ID:wAJPLOxQ
leanをlearnする
11132人目の素数さん
2026/03/13(金) 23:47:11.64ID:P/6qnb7z 出版社:ラムダノート、とあるがそこは、まともな本を出してるだろうか?
12132人目の素数さん
2026/04/01(水) 18:15:43.72ID:1p114+if 国産の定理検証系が必要ではあるまいか?
単なるソフトだけではなくて、CPUやOSや
メモリシステム、ストレージなども含めて、
誤動作やエラーがあってはならない。
OSは極力シンプルに作らねばならない。
OS自身も正しいことを証明すべきだ。
自由に外部割り込みなどが入ると
OSの正しさの証明が困難になるから、
割り込みの機能無しか、プログラムの
特定箇所でだけ割り込みを受け付ける
命令を置くなど。CPUも命令の実行
順序をCPUが動的に入れ替えたりする
とCPUの動作の正しさの検証が難しく
なるから素朴なものにして、レジスター
無しか、あっても1個か2個にする。
CPUにはキャッシュなどは設けない。
メモリは高度のエラー訂正機能を設ける。
ストレージも多重化し、バッファーなど
も正しさの検証を困難にするから辞める。
仮想記憶はやらない。GUIは無しでCUI
だけにする。
CPUも三重化して、CPUに出入りする
データを常に比較して一致している
ことを確かめるハードにする。
違いが出たら、動作エラーを表示し
て停止。電源はノイズを外部から
拾わないように、大容量のバッテリー
で直流給電で動作させる。
外部から電磁ノイズで影響されない
ように、厚い銅板で囲まれた
部屋に置く。室内では照明には直流
点灯のLEDを置くほか、携帯電話の
持ち込みなどは禁止。温度を一定に
保つために、部屋の外から一定
温度、一定湿度の空気をパイプを
使って緩やかに流し入れ流し出す。
できれば宇宙線の影響を避ける
ために地下深くに設置する。
単なるソフトだけではなくて、CPUやOSや
メモリシステム、ストレージなども含めて、
誤動作やエラーがあってはならない。
OSは極力シンプルに作らねばならない。
OS自身も正しいことを証明すべきだ。
自由に外部割り込みなどが入ると
OSの正しさの証明が困難になるから、
割り込みの機能無しか、プログラムの
特定箇所でだけ割り込みを受け付ける
命令を置くなど。CPUも命令の実行
順序をCPUが動的に入れ替えたりする
とCPUの動作の正しさの検証が難しく
なるから素朴なものにして、レジスター
無しか、あっても1個か2個にする。
CPUにはキャッシュなどは設けない。
メモリは高度のエラー訂正機能を設ける。
ストレージも多重化し、バッファーなど
も正しさの検証を困難にするから辞める。
仮想記憶はやらない。GUIは無しでCUI
だけにする。
CPUも三重化して、CPUに出入りする
データを常に比較して一致している
ことを確かめるハードにする。
違いが出たら、動作エラーを表示し
て停止。電源はノイズを外部から
拾わないように、大容量のバッテリー
で直流給電で動作させる。
外部から電磁ノイズで影響されない
ように、厚い銅板で囲まれた
部屋に置く。室内では照明には直流
点灯のLEDを置くほか、携帯電話の
持ち込みなどは禁止。温度を一定に
保つために、部屋の外から一定
温度、一定湿度の空気をパイプを
使って緩やかに流し入れ流し出す。
できれば宇宙線の影響を避ける
ために地下深くに設置する。
2026/04/06(月) 05:12:38.68ID:Nc+CmwqS
国産である必要はない
ハイおしまい
ハイおしまい
レスを投稿する
ニュース
- 【芸能】元和牛・水田信二、離婚を発表 17歳年下・フリーキャスター山本萩子と連名で報告「前向きな決断」 [阿弥陀ヶ峰★]
- 【日中】中国の王毅外相が関係正常化の「条件」を提示 岩屋前外相との会談で ★4 [煮卵★]
- 人口水増しの疑いと総務省… [BFU★]
- 玉川徹氏、アジア大会の金メダルに喜ぶ日本人を分析「GDPで負けている。だからトップになれたら嬉しいと思う状況にあるのではないか」 [muffin★]
- 【中日】井上一樹監督「僕は辞任します」目を潤ませる 3年契約2年目で苦渋の決断「けじめとして…責任を取る決断に至った」 [muffin★]
- 「金ある人だけ助かる」医療現場のファストパス導入にミュージシャン警鐘「政治がクソだとここまで」「ほんまに全員本気出した方がいい」 [muffin★]
- 【悲報】高市早苗、食料品消費税減税のためレジ改修などに1119億円ぶちこむwwwwwww [834922174]
- 高市早苗はヒトラー🪰14 [784319933]
- 日本人「日本は日本だけでやっていけます。中国のモノは0でも成り立ちます。岩屋に騙されるな」反論できる? [511917482]
- 【悲報】亜月ねね先生、ケンモメンに着払いで生きたクワガタを送り付けられる [347751896]
- 【速報】岩屋首相、王毅外相に続き中国副首相とも会談 [329271814]
- マクドナルド行こ🥺