To be a better programmer, write little proofs in your head

To be fair you're picking an example that's extremely finicky about indices. It's probably the hardest basic algorithm to write down without errors. Up there with Hoare partition.

I knew about the infamous Binary Search bugs in books, and I dared to write the first bug-free implementation in my book, very carefully. Still, it ended up having bugs. :) Luckily, Manning's early access program let me fix them before printing.

The C++ standard library phrases binary search as a partitioning problem - finding the index where a predicate goes from false to true, which is helpful for me.

What are the odds you write a binary search that you'll use more than once instead of just running it and writing down the result?

A research paper from Google in 2006 noted that "almost all" binary search (and merge sort) implementations contain a bug (and had for decades), so 90% seems impressive in the face of that.

https://research.google/blog/extra-extra-read-all-about-it-n...

The objective is always to attain some kind of synergy between the business logic and, as others have said, algorithm simplicity. The best way to go about it is to start from the chosen language/environment/library, and build out a DSL that can express the business rules. That's the basic premise of DDD, but where all this got complicated is splitting into contexts and the translation between their boundary.

I believe programmers should learn a bit about programming language theory, mostly the bits about what is a language. Then how to recognize the things behind the labels, and how they morph (either from an operation or from a translation between contexts). Then it's a matter of using the knowledge to move from the environment to a DSL that can express the business rules.

Architecture is the draft for the above, defining the starting point and a direction. And design is where you start to make decisions following the plan. For someone that have an idea of the destination, they can judge both.

I think we're still at the stage of "this team lead makes shit happen" rather than "this strategy makes shit happen," with a lot of the nuances being fuzzy and/or wrong.

Tossing out a few observations:

1. People make mistakes. Your strategy needs to account for that (resilient runtime, heavy type-checking, convenient and often-used REPL, etc).

2. Above a certain project size, nobody remembers everything. Your strategy needs to account for that (excellent multifaceted documentation, disallow long-range interactions in your code, etc).

3. Dependencies have a vastly higher cost than you expect, even in the short term. Plan for that (vendor more things, in-house more things, allocate resources to dependency management, cut scope, etc).

I could go on. The core point is that certain properties of projects are "plainly" true to most people who have been around any length of time. I don't think we're yet at a point where we can often predict anything meaningful about some specific new technology, but a mental framework of "this succeeded/failed _because_ of {xyz}" helps tremendously in figuring out if/how that new idea will fit into your current workplace.

Have to strongly disagree here. I don't think the OP meant thinking up a complete, formal, proof. But trying to understand what kind of logical properties your code fulfills - e.g. what kind of invariants should hold - will make it a lot easier to understand what your code is doing and will remove a lot of the scare factor.

The most basic idea of a proof is an argument for why something is true. It’s not about avoiding small mistakes, it’s about getting directionally correct.

There is no substitute for writing correct programs, no matter how hard it is. If you want correct programs you have to write them correctly.

Turn your first paragraph on its head:

Appropriate abstractions (i.e., "idiomatic code for the language and codebase") make program verification easy. If you are hand-weaving an appropriately-abstracted program, there's little benefit to thinking about loop invariants and pre-post conditions, since they don't exist at that level of generality: correct proofs follow directly from correct code.

Could you elaborate on those techniques from competitive programming please. Genuinely interested! :)

A part of "being a good developer" is being able to evolve systems in this direction. Real systems are messy, but you can and should be thoughtful about:

1. Progressively reducing the number of holes in your invariants

2. Building them such that there's a pit of success (engineers coming after you are aware of the invariants and "nudged" in the direction of using the pathways that maintain them). Documentation can help here, but how you structure your code also plays a part (and is in my experience the more important factor)

I think your frustration is illustrative, actually: the reason mutable global state is bad is because in order to prove that a piece of code reading it is correct, you have to know what _the entire rest of the program_ is doing.

If, instead, you make the global variable immutable, make the state variable into a function argument, or even wrap the mutable global state in some kind of helper class, then you only need to know what the callers of certain functions are doing. The visibility of those functions can be limited. Caller behavior can be further constrained with assertions inside the function. All of these (can) make it easier to prove that the reader is correct.

I think most programmers already do this, actually; they just don't think of their decisions this way.

> It's much harder to prove stuff this way when you call foo(), bar() and baz() across unit boundaries, when they modify global state and are written by different developers.

I think this reinforces the article's point.

Code like this is much more likely to contain bugs and be harder to maintain without introducing more bugs, than programs written from the outset with this goal of "provability".

> when they modify global state and are written by different developers.

Once cancer has metastasized, the treatment plans are more aggressive and less pleasant. The patient can still be saved in many cases, but that depends on a lot of external factors.

Even then, you can get a map of "safe" and "unsafe" locations in the codebase, I.e. you can get a mental model of which functions modify global state and which don't.

Those notes are great, David Liu seems while a wholesome dude https://www.cs.toronto.edu/~david/research.html

The article does include those.

[dead]

I am not a fan of Test Driven Development, not at all.

Having your invariants and pre/post conditions correct is not enough. You also need to do the right thing. For example, you have a function that adds two durations in the form hh:mm:ss, you have mm <= 60 and ss <= 60 as an invariant, testing it is a good thing, but it won't tell you that your addition is correct. Imagine your result is always 1s too much, you can even test associativity and commutativity and it will pass. Having these correct is necessary but not sufficient.

Problem is, when you write tests first, especially tight, easy to run unit tests, you will be tempted to write code that pass the tests, not code that does the right thing. Like throwing stuff at your tests and see what sticks.

I much prefer the traditional approach of first solving the problem the best you can, which may of may not involve thinking about invariants, but always with the end result in mind. And only when you are reasonably confident with your code, you can start testing. If it fails, you will have the same temptation to just pass the test, but at least, you wrote it at least once without help from the tests.

Maybe that's just me, but when I tried the "tests first" approach, the end result got pretty bad.

A test is not a proof, and you can prove something works without ever even running it. There are also properties of a system which are impossible to test, or are so non-deterministic that you a test will only fail once every million times the code is executed. You really need to just learn to prove stuff.

The most complex piece of code I have ever written, as a relevant story, took me a month to prove to everyone that it was correct. We then sent it off to multiple external auditors, one of which who had designed tooling that would let them do abstract interpretation with recursion, to verify I hadn't made any incorrect assumptions. The auditors were confused, as the code we sent them didn't do anything at all, as it had a stupid typo in a variable name... I had never managed to figure out how to run it ;P. But... they found no other bugs!

In truth, the people whom I have met whom are, by far, the worst at this, are the people who rely on testing, as they seem to have entirely atrophied the ability to verify correctness by reading the code and modeling it in some mathematical way. They certainly have no typos in their code ;P, but because a test isn't a proof, they always make assumptions in the test suite which are never challenged.

TDD is also great for playing around with ideas and coming up with a clean interface for your code. It also ensures that your code is testable, which leads to improved readability.

You'll know quickly where you're going wrong because if you struggle to write the test first, it's a symptom of a design issue for example.

That being said, I wouldn't use it as dogma, like everything else in CS, it should be used at the right time and in the right context.

Took the course last year, and I started to appreciate it more while taking functional programming lmao