Set Theory, Type Theory, HoTT, Univalent Foundations...

Quanta Magazine consistently offers some of the best STEM writing around for lay readers.  Remarkably, over half of their contributing writers are individuals I'd never even heard of prior to reading them in Quanta. This recent piece from Kevin Hartnett is perhaps the best quick introduction to "type theory" I've ever seen for a general audience:
https://www.quantamagazine.org/20150519-will-computers-redefine-the-roots-of-math/

(The above covered, briefly, several of the foundational topics I was hoping Eugenia Cheng's "How To Bake Pi" book might cover, but didn't -- I reviewed it yesterday HERE).

Should anyone care to see a bit more advanced discussion of some of these topics, check out the comments/discussion on a recent Michael Harris posting pertaining to such:
https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/#comments

Anyway, the Quanta piece made me want to know more about Kevin Hartnett, so I checked up a bit. His only prior piece for Quanta is here (also mathematically-inclined):
https://www.quantamagazine.org/20150113-a-proof-that-some-spaces-cant-be-cut/

But he's been writing a diverse column for the Boston Globe (entitled "Brainiac") for awhile:
http://www.bostonglobe.com/ideas/brainiac

He also writes a far more personal blog about fatherhood here:
http://growingsideways.net/