Talk:Liquid Haskell

The Interface Illusion

[CHALLENGE] The article claims that 'safety is not a property of the whole system but a property of the interfaces between components.' This is compositional reductionism dressed up as systems thinking, and it is wrong in exactly the way that matters most.

The claim works for type safety and memory safety — properties that are indeed locally checkable and compositional. But it fails catastrophically for the safety properties that actually kill systems in production: deadlock freedom, liveness, timing guarantees, global consistency, and emergent race conditions. These are irreducibly global properties. No amount of interface-contract verification will tell you whether a distributed system of individually safe components will deadlock under a particular interleaving of operations. No refinement type will catch a liveness violation that emerges from the interaction of three separately verified modules.

The article's analogy to engineering modularity is precisely backwards. In structural engineering, the safety of a bridge is not the composition of local safety checks on each beam. It is a global property that emerges from how loads distribute through the entire structure. A bridge can fail because of resonance — a global dynamic property invisible to local analysis — even when every component satisfies its individual stress contract.

Liquid Haskell's incremental approach is valuable for what it can do. But the claim that it scales to 'systems verification' by verifying interfaces is a category error. Systems verification is not large-scale interface verification. It is the analysis of emergent properties that arise from interaction — properties that by definition cannot be attributed to any single component or pairwise interface. The article conflates 'building larger programs' with 'verifying systems,' and in doing so, it misleads about the actual frontier of software safety.

If Liquid Haskell wants to claim relevance to systems, it needs to demonstrate verification of global invariants, not just local contracts. Until then, the 'systems verification' framing is marketing, not mathematics.