Hacker News Reader

Comment by Animats | Hacker News Reader

I wish we had tools for proving object invariants widely available. But such tools tend to come from people pushing their latest type theory or functional programming or something. They're too complex and abstract for most programmers. I tried to fix this once, but it was too soon in the early 1980s.[1] (That was before objects. We would have had object invariants if objects had existed back then. We had function invariants and module invariants.)

This stuff is useful is when you have lots of modifiable data structures which need to be consistent. Window managers. Operating systems. Game engines. Database internals. Most of the things you need to prove are trivial. But you need tools to check that invariant A is maintained by code far distant from where invariant A is defined. Maintenance programmers will miss that.

[1] http://www.animats.com/papers/verifier/verifiermanual.pdf

View on HN

This is usually one of the first things I try to add to projects that have stranded because of reliability issues or because there is code that nobody dares to touch for fear of upsetting some fragile balance.

It can be quite a bit of work but the pay-off can not be over-estimated.

because there is code that nobody dares to touch for fear of upsetting some fragile balance.

Exactly. Where invariants pay off is maintenance. The original programmer intent has been forgotten and is not visible in the code.

I know a big project which hit this wall. There's delicate C++ code with internal inconsistency bugs, and the company can't fix them.

The problem is that the programmers there can't make a ratchet: a monotonously improving codebase where each commit is like the click of a ratchet. If you know your invariants hold then it is fairly easy to establish whether or not a change is an improvement.

Testcases can supply this function, as well as counters set up for that purpose (statsd or something to that effect).

Once you have enough of those you can (slowly) start to make changes to observe the effects, and once you understand the codebase add more invariants that you have now determined should exist.

The last project where I took that approach (about 4 years ago now) went from 'intractable' to 'stable' in a relatively short time but it required a lot of thinking and some really hard work to get it there.

Much better if your language/platform supports that sort of thing out of the box, even better if it can be done across subsystems.

Can you give a few examples on what exactly did you do?

I am a big proponent and a fan of gradual refactoring -- even if you simply add a feature that can be forced in (which I never do).

But I am always to open learn some more techniques. And I have to admit with a heavy heart that I never really studied computer science... :(

(Planning to fix that but still have no idea where to even start.)

The poorly named but very interesting "hypothesis"[0] is a quickcheck implementation (extension?) for python that might provide the "easy" access to these tools that you're looking for.

[0] https://hypothesis.works/

Why is it poorly named? I've always liked it.

So, I also really like it from a "cool statistics reference" point of view. However, I don't think it is informative, unique or google-able, and discoverability is pretty important imho.

Is there a viable solution that isn't type theory or functional programming or something? If it were feasible to do so, wouldn't we see progress in "everyday" common language?

There was for Modula III. DEC SRL in Palo Alto did a nice verification system for Modula III. But Modula III went down with Digital Equipment Corporation.

C/C++ has too much undefined behavior. Ada died off. The scripting languages don't need it as much. Rust had potential for proof work, but went off in a different direction. There are modern proof systems, but they're rarely integrated with the programming language.

I thought the legacy of Modula-3 lives in OpenJML (through ESC/Modula-3 -> ESC/Java -> ESC/Java2 -> OpenJML)? I have never heard anyone use it though.

"Ada died off. "

On the verification side, it's never had more users that I'm aware of. SPARK and Frama-C are very active compared to almost non-existent use of formal methods in industry decades ago. Rust could similarly have a subset integrated with Why3 platform to make the formal methods easier to use. Further, I've seen extraction done from Coq to C and Rust. There's also one person modeling C in WhyML to write the algorithms in the latter but extract to former. Or something like that. Could be done for Rust, too.

> Rust had potential for proof work, but went off in a different direction.

Which direction is that?

I think Dafny is an interesting approach - https://www.microsoft.com/en-us/research/project/dafny-a-lan...

The C++ type system is essentially a functional programming language, and it seems to have developed independently, indicating to me that there is something fundamental about functional programming. It turns out this has not just occurred to me and there is a deep relation between mathematical proof and functional expressions. Thus, if you are trying to prove anything logically, you will likely eventually end up with some kind of functional-looking notation or something that is very closely related.

For some reason, the moment you bring up mathematical thinking, most programmers shy away and claim that this isn't something they should work with 'everyday'.

I blame the lack of visibility of the accessible material... which I am still looking for. Any suggestions?

I never studied CS and I deeply regret that now. I want to up my game and I don't want to always just patch stuff around to infinity, but I honestly have no idea where to start.

Cleanroom just uses functional decomposition, the simplest of the control flow primitives, and math you learned in middle or high school. Got results on lots of projects.

http://infohost.nmt.edu/~al/cseet-paper.html

https://pdfs.semanticscholar.org/12d5/23e586ffde5cbe020cb3fa...

(Second link has a table and description showing the results they got. Stavely's book distills it into lightweight, less-processy form.)

Design by Contract itself is like assertions on steroids. If your language lacks support, you can build it into your functions at beginning, middle and end. If OOP language, you might use constructors and destructors. If trying to understand it, I have a link that you can give even to project managers.

https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b...

One benefit of making it a formal spec is you can generate tests directly from your specs. This is an old, old technique being rediscovered recently. Various names include specification-based, model-based, contract-based, and property-based test generation. The last thing you can do is manually or automatically convert your specs into runtime checks for the above and/or fuzz testing. The failure takes you exactly to the property that failed if it was one of them.

Finally, for just the most critical things, you can try formal proof on them. SPARK Ada is a great example used in industry with the book being pretty easy to follow.

https://www.amazon.com/Building-High-Integrity-Applications-...

The nice thing about that toolset, esp the proprietary version, is that you can use automated provers to avoid having to do mathematical proof by hand. If something doesn't pass, you have several options: do some manual work on hints to the automated provers or actual proofs in a proof assistant; monkey around with the code to see if different structure or algorithm gets it through; put in runtime checks for just the properties you couldn't prove. If you do the last one and keep programming while solvers run, then the productivity is similar to Design-by-Contract with the extra benefit some properties might hold in all cases. You might also get performance boost by reducing unnecessary, safety checks via proofs that were successful.

> Is there a viable solution that isn't type theory or functional programming or something?

What's so wrong with functional languages? I am sure you have heard this cliche a lot but here it comes once more -- I became a much better programmer once I learned an FP language.

Still, back in my Java days I achieved this with a ton of defensive coding, always doing deep cloning before passing complex data structures to anywhere, and trying to enforce design by contract (interfaces and their implementation classes)... which are practically the patterns that any average FP language uses: pattern-matching, immutability and always copying data and thus never passing stuff by reference (always by value), and behaviours / protocols / macros (of the manipulating the AST kind, not in the way C does it).

So to be fair, you are bound to land at an FP language eventually. Maybe you just don't know it yet. Which is fine, learning is about the journey and not the destination anyway.

Reply on news.ycombinator.com