[mbrock]

Dependent type systems are one way to verify logical constraints in code, but not the only way. Look at Dafny for a good example of how checked invariants can be integrated into an ordinary imperative language. Or ESC/Java for the same approach but integrated into Java. The basic technique goes back at least to Dijkstra’s predicate transformers and nowadays the verification is mostly automatic with SMT solvers.

[bjz_]

Those can be integrated with dependent types too - for an example look at F*.