3 ms·

> Provably correct software is possible. Ah cool, so you've solved the halting problem then?

• weavie 10y ago
  They didn't say it had to be Turing complete.
  • DanWaterworth 10y ago
    It's not about turing completeness. Deducing arbitrary properties of programming written in primitive recursive languages is also undecidable. This is why type inference in dependently typed languages is undecidable.
• DanWaterworth 10y ago
  You don't need to solve the halting problem to write provably correct software (that is, software that conforms to a formal specification). The halting problem (and Rice's theorem) come into play when you are trying to deduce things about arbitrary programs written in turing complete languages. It's like the difference between being able to express proofs in maths, versus having a method of deciding the validity of arbitrary propositions. We can certainly write programs that we can we can prove things about, but given an arbitrary program, we can't always tell whether it will do the right thing.
• lmm 10y ago
  It was "solved" in 1940 (proven in 1967) by the simply typed lambda calculus.