> 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.
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.