It would be an interesting future in which Koka[1] becomes the new Python. Or Lean 4,[2] and we end up with formally proved ML code in 2043. [1] https://koka-l

It would be an interesting future in which Koka[1] becomes the new Python. Or Lean 4,[2] and we end up with formally proved ML code in 2043. [1] https://koka-lang.github.io/koka/doc/index.html https://koka-lang.github.io/koka/doc/index.html [2] https://leanprover.github.io/documentation/ https://leanprover.github.io/documentation/