LANAが形式化に失敗した理由は、はっきり言って、
理解者以外の人がやってるからじゃねーか？
だってIUTグループ内ではLean code（非公開）が
すごく役立ってるらしいっすよ
https://aitpm.github.io/
>The skeletal Lean code that we wrote for this portion of IUT
>constituted a remarkably successful case of the use of Lean
>as a communication tool.

あれだよ、あれ
零と交信できるとか透視できるとか主張する人によくあるやつ
科学的にきっちり管理された状況で再現してみせてって
言われても、ノンビリーバーがいる環境じゃあ
そのせいでできなくなっちゃうってやつ

あるいはマジシャンが気分よく手品ショーやってんのに、
無粋な客が、タネを隠してるところを開けて見せろって
しつこく言って興ざめするやつ