Virtual Machines, Dynamic Compilers, and Implementation Frameworks make dynamic languages easier and more efficient to optimize. Meanwhile, IDEs, provers, dependent types, type inferencers, and (so-called) “generative AI” mean programmers can express - statically - more information about the dynamic behavior of their programs. Component libraries in these languages will come with assertions and proofs of their behavior, and their advocates fantasize about transforming programming into the composition of dependently-typed higher-order yoneda morphisms, ensuring programs are correct-by-construction (where that construction is carried out by yet more generative AI).

In this talk, I’ll speculate about what the resulting world will be like for programmers. Rather than a static world of platonic mathematical abstractions, I argue that the opposite will be true: that all languages will be dynamic.