And yet MLTT led to Coq, Agda, Idris and Lean, while your ”PL practice” approach sounds like it would lead to, well, Go.