I think a language like that could be great if you managed to synthesize all the good parts into a modern whole. I always liked the very pragmatic mechanism, i

I think a language like that could be great if you managed to synthesize all the good parts into a modern whole. I always liked the very pragmatic mechanism, in Wirth's languages and in Ada, of attaching constraints to data types; for example, defining a type as an integer of range 1..9. On the one hand, from a type-theoretical viewpoint, it's completely cheating — the mechanism is hardwired into the language, there's no real underlying system or symmetry to it, unlike a proof-based language such as Idris or Agda. On the other, it's awfully pragmatic.