2 ms·
How were weak and strong defined in the literature you read? Anyway, more on soundness. I can recommend a couple papers: Wadler (inventor of the monad) wrote
by TheDong 7y ago
How were weak and strong defined in the literature you read?
Anyway, more on soundness. I can recommend a couple papers:
Wadler (inventor of the monad) wrote a paper called "Well-Typed Programs Can’t Be Blamed" [0] about soundness.
There was a recent paper that made the rounds about how java's type-system is provably unsound as well that's worth reading [1].
I second the parent comment that weak and strong are ill-defined in my experience, while sound/unsound have well-accepted definitions and are commonly used in academia. Your experience obviously differs for whatever reason.
You can find many other references to soundness in the citations of those papers, as well as scattered around the internet.
[0]: https://link.springer.com/chapter/10.1007%2F978-3-642-00590-9_1 https://link.springer.com/chapter/10.1007%2F978-3-642-00590-...
[1]: https://dl.acm.org/doi/10.1145/2983990.2984004 https://dl.acm.org/doi/10.1145/2983990.2984004