4 ms·
It doesn't matter if the language defines the behaviour of, say, offsetting an array beyond its declared bounds. That doesn't change the general undecidability
by caf 9y ago
It doesn't matter if the language defines the behaviour of, say, offsetting an array beyond its declared bounds. That doesn't change the general undecidability of statically proving the offset will always be within the bounds at compile-time - in other words, you need runtime checks in some cases (it's just a matter of whether the compiler or the programmer supplies them).
- eru 9y agoNah, with some help from the programmer, you can produce those proofs. It's not too hard. The halting problem is impossible to solve for arbitrarily evil programs, but that doesn't mean that it's impossible to write programs that are easy to analyse.
- gpderetta 9y agoI think that statically guaranteeing something like in-bound indexing or absence of division by zero you need depended types, which is not exactly easy nor mainstream. And even with dependent types, many non-evil, otherwise correct programs will be rejected.
- yorwba 9y agoAren't dependent types able to express any statement formalizable in predicate logic? This should include most things you might want to say about the correctness of non-evil programs. I think the real problem with them is that type-checking itself becomes undecidable, so you get the additional problem of proving that your program is indeed correctly typed.
- eru 9y agoYes, for the general problem you want dependent types (or similar). There are middle grounds, of course: you can let the compiler figure out on its own what it can, and let it insert runtime checks for the other cases. And add some way for the programmer to declare that eg "warn me if this can't be optimized" or "trust me, this is safe" or even "here's a proof for you". But in any case, dependent types are possible---undecidability is not a hard barrier here.
- tom_mellior 9y agoHere are two nice blog posts on the state of the art of this "not too hard" problem: https://maniagnosis.crsr.net/2017/06/AFL-brute-force-search.html https://maniagnosis.crsr.net/2017/06/AFL-brute-force-search.... https://maniagnosis.crsr.net/2017/06/AFL-bug-in-quicksearch.html https://maniagnosis.crsr.net/2017/06/AFL-bug-in-quicksearch.... Possible? Yes. Too time-consuming and fiddly for the economic realities of 99.9% of all programmers? Yes, that too.
- pjmlp 9y agoThe economic realities would be quite different if software companies were legally accountable for their defects, just like in many other industries.
- eru 9y agoThat would mostly mean that only big companies that can afford a herd of lawyers would be able to produce software. At least that how bank regulation works out in practice.