orange @[email protected]

「渋谷行きの電車の運転士が、回送電車の後部が進行方向の線路にはみ出しているのに気づき緊急時用の無線を発信、無線を受信した回送電車は車両を動かせなくなり渋谷行きの電車も非常ブレーキをかけたものの間に合わず衝突したということです。」

東急田園都市線事故　一部区間の運転見合わせ続く　復旧には長時間｜日テレNEWS NNN https://news.ntv.co.jp/category/society/96b2da159dca402282a71a007dd867cf

防護無線飛ばしたのは衝突した上り普通列車らしいっす

眉に唾を大量につけながら見てほしんだけど…もしこんな「そんなことあるゥ！？」なことが東急田園都市線梶が谷駅で起きてしまったとすれば…

すべて正常動作した状態で進路開通できてしまう…

ちゃんと書いた。

なので、梶が谷駅の設備は本当に健全だったのか、という疑いが出てしまい、たとえ脱線した車両を撤去できたとしても、ちゃんと情報を集め切るまで再開はムリでは？というわけ。

腑に落ちないのは、ふつうは軌道回路（車両の存在を検知する回路）はこんな感じで分割して、そのうち問題の赤で示した部分に車輪が載っていた場合は、上本→3番の進路は構成できないようインターロックがかかっているはず、というので…

運転士が見習いだろうが、停止位置が間違ってようが、これが安全を担保するための原則のはずなのに、実際は赤の部分にまだ車両が居たのに3番への進路が開通してしまったという…

全部コンパイラに自動でやらせようとするから悪い　プログラマが証明を書け！

もちろんこれは危険なメモリ操作を「自動で」検出しようと考えた場合なので、「プログラマが安全性の形式的証明を手動で書かない限り全て危険とみなす」なら可能だと思う

整数オーバーフローくらいなら……いやどうなんだろ、結局篩型みたいなの使う羽目になって SAT/SMT の計算量が嫌すぎる〜みたいな話になるか？

文脈わからないけど、たとえばチューリング完全な言語では無限ループがないことの証明はできない (停止性問題)

「どれだけコンパイラが賢くても、警告し切れないケースが存在する」ことは数学的に証明できそうな気がする

今の軌道回路の設計ってどうなってるんだろうねえ、分岐器のない本線上は無絶縁にして減衰考慮で設計っていう考えで合ってるとは思うんだけど、分岐器のある駅構内までそれやっちゃうとしっちゃかめっちゃかになるので、信用ならない技術使うのではなくて単純に絶縁してると思いたい…

東急は「回送の停車位置が不適切だった可能性」を挙げているらしいけど、そんなヒューマンエラーで即詰むような安全装置ってなんやねんというのはある…