Post #3095769

Just read through https://daniel.haxx.se/blog/2026/04/22/high-quality-chaos/ I've reached the point where I don't think it matters what programming languaeg you use to solve a given job. Use untyped lambda calculus for all it matters. Your type-checking problem has extended beyond the boundaries of what we think of as belonging to programming languages. At this point, people need to be talking about invariants. "Principle of least surprise" is a soft invariant. "Must not write past the end of the buffer" is an invariant. "Must not write to memory or storage not set aside for the purpose" is a higher-order invariant--a dependently-typed one. More on this later. There's a real risk of waterfall-style planning, but I don't think it has to be that way.