> "This doesn't have a formal meaning, therefore it's not useful" is quite a logical leap you've got there.
It means that everyone defines strong and weak in their own way, which has happened in every type system debate I've seen over the past 15 years.
> "Soundness" certainly gives stronger guarantees, but it's more than I've needed.
Soundness is exactly the metric you need. Either you can rely on your type system not to lie to you, or you can't.
Programming language expressiveness means "Felleisen expressiveness". It's a metric approximated by source code compression, which is why the great programming shootout includes gzip metrics for source programs.
> It means that everyone defines strong and weak in their own way, which has happened in every type system debate I've seen over the past 15 years.
Okay, that's fair. Part of the reason I gave examples and defined the spectrum I was talking about was to address this problem, because I know people don't necessarily know what I'm talking about.
It means that everyone defines strong and weak in their own way, which has happened in every type system debate I've seen over the past 15 years.
> "Soundness" certainly gives stronger guarantees, but it's more than I've needed.
Soundness is exactly the metric you need. Either you can rely on your type system not to lie to you, or you can't.
Programming language expressiveness means "Felleisen expressiveness". It's a metric approximated by source code compression, which is why the great programming shootout includes gzip metrics for source programs.