Hacker News Reader

Comment by dnautics | Hacker News Reader

Because in mathematical proofs the preconditions are usually explicit and well understood. A program usually has reality-bound constraints that are not explicit, e.g. "does not work unless the target system has at least 3.5mb of memory" or "assumes that opcode X never fails" or "assumes memory is consistent and never is corrupted"

View on HN

Programs could be explicit about those constraints, encode more of them statically and check them statically.

Everything has a failure rate. This introduces another set of heuristics (and another false-{positive,negative} rate), another set of potential implementation bugs in those heuristics. What if being able to run the program on a particularly memory-limited computer could save the universe, even more slowly than the project manager originally wanted it to run?

Statically encoding something like a memory constraint sounds very hard for all but the simplest algorithms. What about a randomized algorithm that sometimes uses more heap? How do you get around not knowing how much it's going to use without running it?

Allocate for the worst case use in the bss. The program's static size indicates explicit memory requirements.

That's Design-by-Contract. On checking side, one can generate tests from specs, static analysis, turn them plus code into verification conditions to feed to solvers, or inputs to theorem prover for handling complex stuff. Eiffel implements DbC with test generation. SPARK Ada does automated and manual proofs. Ada 2012 added contracts but idk tool support. Many languages have ways of emulating this functionality, too.

What you're describing is essentially a proven, lightweight, formal method for improving software quality. Many commercial apps use it.

indeed, very few programming languages actually do that, and you're probably running the language on top of another language that has flawed guarantees on those constraints. Or hardware. How do you guarantee your program hasn't gone rogue if you can't guarantee the bits in your memory.

Yeah, this would be the question for fault tolerance and the whole world of distributed systems that inevitably comes with it.

i think the reasons pointed out in the post and many comments here on HN are more of the cause,

but another reason is that code often has to be written in a shorter time frame. there are tools like coq that enable people to write code that is correct by proofs, but I'd hate to do my daily work that way

Reply on news.ycombinator.com