I look back at the module systems we considered so far (Haskell's, Standard ML's, and Agda's), and consider a few points that are on my mind about these. I also mention a few other languages' module systems (Clojure, Java 9). I also ponder names and namespace management.
The podcast Iowa Type Theory Commute is embedded on this page from an open RSS feed. All files, descriptions, artwork and other metadata from the RSS-feed is the property of the podcast owner and not affiliated with or validated by Podplay.