Yes, there has been much progress in module systems. The very Bob Harper mentioned there was involved in the design of the SML module system, which is often cited in the CS literature as `the' reference module system. SML achieves a level of isolation that is simply impossible to achieve in a language like Java or Smalltalk. in Java, any object you can still call `hashcode()' and `toString()' etc. on, and it's often possible for someone to subclass one of your internal classes and thereby break your intended module structure.
In SML, you can confine types through (e.g.) the following signature:
(* this is imperative code; a typical SML program focuses on functional code, but it's good enough for illustration purposes. *)
signature STACK =
type 'a stack (* 'a is a type parameter, so "'a stack" is what OO-land calls a `generic type' *)
empty : unit -> 'a stack (* create fresh stack *)
push : 'a stack -> 'a -> unit (* take a stack of 'a elements, take an element of type 'a, and plug them together *)
pop : 'a stack -> 'a option (* "'a option" means that the operation may fail *)
You can then implement this stack in various structures that match this signature, and confine it in such a way that only the operations listed above are available. That is, you can't stringify stacks (there is no such operation listed there, though you can choose to add one), you can't compare them (again, no such operation), you can't `reflect' on them and you can't access their `protected' functionality by subclassing them, unless the stack implementer put a separate view of the structure into place for that particular purpose.
Why is this good? Client code won't end up using features that you didn't want to expose. Why is it bad? If you forgot to expose something important, someone else will have to re-implement it. But that's your fault, then, not the language's fault.
SML also allows you to build modules from other modules through something called `functors', but let's leave that for another time.
Now, SML's modules have issues-- you can't have mutual dependencies between them (which does have advantages, too, though), and the question of how to integrate type classes (something you may know as `C++ concepts') is unresolved. But the concepts behind the module system are clear and powerful. So if you want to teach the concepts underlying modular software design, this is a vastly better choice than most other options out there. (I remember the Modula-3 module system being fairly good, too, but not quite at this level.)
So, for teaching purposes I'd say Bob Harper is closely connected to the best system out there that has actual working implementations tied to it.