All Languages Are Dynamic (Invited Talk)

Abstract

Virtual Machines, Dynamic Compllers, and Implementation Frameworks make dynamic langauges 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 behaviour of their programs. Component libraries in these languages will come with assertions and proofs of their behaviour, and their advocates fantasise 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.