News for hackers. Stuff that matters.

A comment on Undebt: How We Refactored 3M Lines of Code. Parent comment

Re:Undebt: How We Refactored 3M Lines of Code by lmm on Wednesday August 24, 2016 @05:12AM (#12350702)
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.

[ Parent | on HN ]
Re:Undebt: How We Refactored 3M Lines of Code by bennofs on Wednesday August 24, 2016 @06:13AM (#12350914)
> 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.

[ Parent | on HN ]
Re:Undebt: How We Refactored 3M Lines of Code by DanWaterworth on Wednesday August 24, 2016 @06:21AM (#12350944)
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.
[ Parent | on HN ]
Re:Undebt: How We Refactored 3M Lines of Code by jbergens on Wednesday August 24, 2016 @05:32AM (#12350760)
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...
[ Parent | on HN ]
Re:Undebt: How We Refactored 3M Lines of Code by chimprich on Wednesday August 24, 2016 @05:27AM (#12350749)
> Provably correct software is possible.

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

[ Parent | on HN ]
Re:Undebt: How We Refactored 3M Lines of Code by DanWaterworth on Wednesday August 24, 2016 @06:06AM (#12350880)
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.

[ Parent | on HN ]
Re:Undebt: How We Refactored 3M Lines of Code by lmm on Wednesday August 24, 2016 @06:09AM (#12350894)
It was "solved" in 1940 (proven in 1967) by the simply typed lambda calculus.
[ Parent | on HN ]
Re:Undebt: How We Refactored 3M Lines of Code by weavie on Wednesday August 24, 2016 @05:42AM (#12350783)
They didn't say it had to be Turing complete.
[ Parent | on HN ]
Re:Undebt: How We Refactored 3M Lines of Code by DanWaterworth on Wednesday August 24, 2016 @06:09AM (#12350891)
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.
[ Parent | on HN ]