アカウント名:
パスワード:
これはファイルシステムみたいなlow levelのコード全体の形式的証明に成功したって話であって、現実的にデータ損失が発生しないって話じゃないでしょ。
たとえば現実のハードディスク中のfirmwareは、今回の形式的証明で担保されてないわけで、この間のストーリー http://hardware.srad.jp/story/15/08/26/0642232/ [hardware.srad.jp] にあったような、firmware に原因がある silent data corruption には対処できない筈。
「形式的」って数学用語なわけだが「実質的」の対義語みたいに見えてしまっていまいちな訳だと思う。
適当な用語が望まれますね!
「適当な」とか「勝手な」とか「任意の」と訳されるアレも何とかしてほしい。
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
私は悩みをリストアップし始めたが、そのあまりの長さにいやけがさし、何も考えないことにした。-- Robert C. Pike
形式的証明の話でしょ (スコア:0)
これはファイルシステムみたいなlow levelのコード全体の形式的証明に成功したって
話であって、現実的にデータ損失が発生しないって話じゃないでしょ。
たとえば現実のハードディスク中のfirmwareは、今回の形式的証明で担保されてない
わけで、この間のストーリー http://hardware.srad.jp/story/15/08/26/0642232/ [hardware.srad.jp] に
あったような、firmware に原因がある silent data corruption には対処できない筈。
Re:形式的証明の話でしょ (スコア:0)
「形式的」って数学用語なわけだが「実質的」の対義語みたいに見えてしまっていまいちな訳だと思う。
Re:形式的証明の話でしょ (スコア:1)
適当な用語が望まれますね!
Re: (スコア:0)
「適当な」とか「勝手な」とか「任意の」と訳されるアレも何とかしてほしい。