My understanding is that the research background for a lot of dependently typed designs is based on proof theories where the program/proof represents the theory

My understanding is that the research background for a lot of dependently typed designs is based on proof theories where the program/proof represents the theory/constraint one-to-one. Other systems (PRL, Hoare logic) also exist but either have difficulties or haven’t had the same level of research and exploration to reach designs like modern dependently types languages. So you can easily add imperative steps to such a language, but since you not rely on side-effects for “interesting” behavior, it becomes more difficult to match the underlying proof theories to the kind of verification you’re attempting. I’m confident people will flood this comment with sources showing how proof theories exist which don’t have these properties, but I think the prevalence of DT langs nowadays does suggest that this particular synthesis is somewhat more productive so far.