This "static" vs "dynamic" distinction is largely artificial. Every program has parts that make sense to think of as "static" and parts that will be very "dynam

This "static" vs "dynamic" distinction is largely artificial. Every program has parts that make sense to think of as "static" and parts that will be very "dynamic", and the ratio of these two differs from program to program (and even within a program, from day to day). The same goes for making statements about programs. Therefore, in Pyret, we recognize that there are lots of different levels at which we make statements about our programs: from tests through types to specifications, spanning both static and dynamic aspects. They not only aren't in conflict, they're even related. Most languages include only a subset of them or make them appear to be disjoint. In contrast, in Pyret, we're already working on linking these to one another, and are going to keep pushing in this direction. Languages that leave out one or more of these end up forcing users to reinvent these wheels for themselves (because they're each good ideas that people inevitably want). But by forcing people to reinvent a wheel, they end up giving users ad hoc versions of these tools, and also introduce friction between these parts. (E.g., as Robby Findler found several years ago, just about every single bolted-on DBC system had significant limitations or errors.)