> "To the far right, we have a hypothetical language with such a strong type system that, indeed, if it compiles, it works."
> For good measure, despite my failure to understand the implications of the halting problem, I'm otherwise happy with the article series Types + Properties = Software. You shouldn't consider this particular example a general condemnation of it. It's just an example of a mistake I made. This time, I'm aware of it, but there are bound to be plenty of other examples where I don't even realise it.
I don't see what the mistake is. Halting and Godel's incompleteness theorems only say there exists problems where you don't know if there's a solution or not - that's very different from saying you can't come up with solutions for specific problems.
For example, you can't tell if any arbitrary crazy program halts but most loops people code in practice have trivial proofs of halting because it's usually simple loops from 0 to the fixed length of a collection. If some code is full of loops where you're nervous about them halting a lot, there's probably something very wrong with the design that would get flagged in integration tests and during use too.
It's been demonstrated you can statically prove the correctness of something as complex as an operating system for example (see https://sel4.systems/About/) so the above isn't much of a barrier to proving interesting program properties:
seL4's implementation is formally (mathematically) proven correct (bug-free) against its specification, has been proved to enforce strong security properties, and if configured correctly its operations have proven safe upper bounds on their worst-case execution times
> For good measure, despite my failure to understand the implications of the halting problem, I'm otherwise happy with the article series Types + Properties = Software. You shouldn't consider this particular example a general condemnation of it. It's just an example of a mistake I made. This time, I'm aware of it, but there are bound to be plenty of other examples where I don't even realise it.
I don't see what the mistake is. Halting and Godel's incompleteness theorems only say there exists problems where you don't know if there's a solution or not - that's very different from saying you can't come up with solutions for specific problems.
For example, you can't tell if any arbitrary crazy program halts but most loops people code in practice have trivial proofs of halting because it's usually simple loops from 0 to the fixed length of a collection. If some code is full of loops where you're nervous about them halting a lot, there's probably something very wrong with the design that would get flagged in integration tests and during use too.
It's been demonstrated you can statically prove the correctness of something as complex as an operating system for example (see https://sel4.systems/About/) so the above isn't much of a barrier to proving interesting program properties: