Hacker News

points by poly2it 2 days ago | 0 comments

Papers on type soundness from the last 30 years usually explore the domain further than C semantics.

Soundness means that the program behaves in accordance with what its types express. You're right that C may be unsound due to undefined behaviour, but I don't think this is about soundness. What you're saying is that papers on types show how you can use types to express more constraints.

[–] ranger_danger 2 days ago

There can be other valid perspectives and definitions of that word than yours.

I think almost all (tech) arguments stem from simple disagreements and/or different assumptions made on the definition of a (subjective) term.

[–] pron 2 days ago

You may be right in general, but soundness comes from formal logic, where they're pretty fastidious with their definitions. Soundness certainly doesn't mean the expressivity of the types (i.e. what constraints they can represent); it's about the relationship between the runtime behaviour of a program and the types in the code.

[–] ranger_danger 2 days ago

Again I think you're trying to push a specific definition as more correct than OP's somehow. Why not just ask them what they meant to understand their intent/context instead of saying they are wrong?

Unless the point of your argument isn't to understand OP but simply to "win."

[–] pron 1 day ago

I think I understand their point and even said, "What you're saying is that papers on types show how you can use types to express more constraints," and that's correct. I merely pointed out that that's not soundness, which is something I think they'd like to know. There may be some leeway in the definition of soundness and how it's similar to or different from type safety, but either way, type expressivity is something different altogether (and C certainly has issues with both expressivity and type safety or soundness, but they're different issues). So the point isn't to win - the argument was right and I'm not claiming that C's type system is expressive - but to explain the different terms and their meaning in programming languages and formal semantics.

[–] ciefa 2 days ago

Can you link some?

[–] quotemstr 2 days ago

That's not the same as asserting that soundness requires adherence to the current fashion, sum types over results and errors. TIMTOWTDI.

You don't have to think C is sound or good to distinguish a disfavored API style from mathematical unsoundness. There are infinitely many type safe APIs and languages that are, despite their soundness, ugly and hard to use.

Let's not project every dimension along which a language can be good or bad onto the axis of safety.