Hacker News Reader

Comment by lmm | Hacker News Reader

That bug exists because it's written in a language where + is permitted to silently do surprising things, for reasons that made sense as a performance optimization for general-purpose computers in the '70s and embedded systems in the '90s (the original target of Java) but do not make sense for general-purpose computers today.

Better languages are possible. Provably correct software is possible. We really can eliminate bugs.

View on HN

> Provably correct software is possible.

Even then, the software is provably correct according to some specification, which can still have bugs. No technology can fully prevent logic bugs.

You're technically correct, but in practice, proving that software does confirm to a formal specification is, empirically, a good way of drastically reducing defects.

Often when people mention provably correct software what they mean is software that don't crash and always produces output for correct input. It usually doesn't mean that the output is correct...

> Provably correct software is possible.

Ah cool, so you've solved the halting problem then?

They didn't say it had to be Turing complete.

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.

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.

It was "solved" in 1940 (proven in 1967) by the simply typed lambda calculus.

Reply on news.ycombinator.com