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.