[RHSeeger]

> While I prefer expressive type systems by a long shot, I would be much more careful about it "guaranteeing correctness".

Yeah, you're not guaranteeing correctness. There's a quote from automated testing discussions that applies here...

> You're not proving the system works. You're proving that system isn't broken in specific ways

Likewise, for a type system, it's guaranteeing the system is correct for the specific subset of "ways it can be incorrect" that the type system covers.