Neither Kotlin nor any other industry language addresses my original point, namely: > What we need is “a formal semantics for a language, with practical proof

Neither Kotlin nor any other industry language addresses my original point, namely: > What we need is “a formal semantics for a language, with practical proof principles for designing correct programs”. However, I'm not disappointed in industry languages, because I don't actually expect anything from them.