I wonder if there is a rigorous/formal method to identify 'monotonicity' in code? Seems like it should be straightforward...
To be a better programmer, write little proofs in your head
81–90 of 181 posts
Re: To be a better programmer, write little proofs in your head
#82The best way I have found to integrate this approach is Test Driven Development. When done well, every test you write before you see it fail and then you write the barest amount of code that you think will make it pass is a mini-proof. Your test setup and assertions are what cover your pre/post conditions. Base cases are the invariant. The key here is to be disciplined, write the simplest test you can, see the test f…
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 tha…
> A test is not a proof
Actually, a test _is_ a proof! Or more specifically, a traditional test case is a narrow, specific proposition. For example, the test `length([1, 2, 3]) = 3` is a proposition about the behavior of the `length` function on a concrete input value. The proof of this proposition is _automatically generated_ by the runtime, i.e., the proof that this proposition holds is the execution of the left-hand side of the equality and observing it is identical to the right-hand side. In this sense, the runtime serves as an automated theorem prover (and is, perhaps, why test cases are the most accessible form of formal reasoning available to a programmer).
What we colloquially consider "proof" are really more abstract propositions (e.g., using first-order logic) that require reasoning beyond simple program execution. While the difference is, in some sense, academic, it is important to observe that testing and proving (in that colloquial sense) are, at their core, the same endeavor.
Re: To be a better programmer, write little proofs in your head
#83The best way I have found to integrate this approach is Test Driven Development. When done well, every test you write before you see it fail and then you write the barest amount of code that you think will make it pass is a mini-proof. Your test setup and assertions are what cover your pre/post conditions. Base cases are the invariant. The key here is to be disciplined, write the simplest test you can, see the test f…
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 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 t…
You’ve missed the most important point of TDD—and indeed, of tests.
Tests do not ensure that your functions are correct; they ensure that you are alerted when their behavior changes.
Second, TDD is a way to force dogfooding: having to use the functions you’re going to write, before you write them, helps you design good interfaces.
Re: To be a better programmer, write little proofs in your head
#84Earlier quoted context omitted.
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 tha…
> A test is not a proof Actually, a test _is_ a proof! Or more specifically, a traditional test case is a narrow, specific proposition. For example, the test `length([1, 2, 3]) = 3` is a proposition about the behavior of the `length` function on a concrete input value. The proof of this proposition is _automatically generated_ by the runtime, i.e., the proof that this proposition holds is the execution of the left-ha…
That is stretching the definitions of proofs.
assert random() != 0.
Re: To be a better programmer, write little proofs in your head
#85Oh, I have a relevant and surprisingly simple example: Binary search. Binary search and its variants leftmost and rightmost binary search are surprisingly hard to code correctly if you don't think about the problem in terms of loop invariants. I outlined the loop invariant approach in [1] with some example Python code that was about as clear and close to plain English at I could get. Jon Bentley, the writer of Progra…
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?
I once needed to write binary search for a microcontroller in C (no libraries). The routine ran about every hour, with appx 4M data points.
Re: To be a better programmer, write little proofs in your head
#86Earlier quoted context omitted.
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 tha…
Interesting, could you show me a formal proof that can't be expressed in logic (ie. code) and then tested? My thought here is that since proofs are logic and so is code you can't have a proof that can't be represented in code. Now admittedly this might look very different than typical say JUnit unit tests but it would still be a test validating logic. I am not saying every system is easily testable or deterministic b…
Consider a function that gets an array of integers and a positive number, and returns the sum of the array elements modulo the number. How can we prove using tests, that this always works for all possible values?
Not discounting the value of tests: we throw a bunch of general and corner cases at the function, and they will ring the alarm if in the future any change to the function breaks any of those.
But they don't prove it's correct for all possible inputs.
Re: To be a better programmer, write little proofs in your head
#87Oh, I have a relevant and surprisingly simple example: Binary search. Binary search and its variants leftmost and rightmost binary search are surprisingly hard to code correctly if you don't think about the problem in terms of loop invariants. I outlined the loop invariant approach in [1] with some example Python code that was about as clear and close to plain English at I could get. Jon Bentley, the writer of Progra…
[deleted]
Re: To be a better programmer, write little proofs in your head
#88Earlier quoted context omitted.
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 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 t…
You’ve missed the most important point of TDD—and indeed, of tests. Tests do not ensure that your functions are correct; they ensure that you are alerted when their behavior changes. Second, TDD is a way to force dogfooding: having to use the functions you’re going to write, before you write them, helps you design good interfaces.
> Tests do not ensure that your functions are correct; they ensure that you are alerted when their behavior changes.
I agree with that part and I am not against tests, just the idea of writing tests first.
> helps you design good interfaces
I am sure plenty of people will disagree but I think testability is overrated and leads to code that is too abstract and complicated. Writing tests first will help you write code that is testable, but everything is a compromise, and to make code more testable, you have to sacrifice something, usually in the form of adding complexity and layers of indirection. Testability is good of course, but it is a game of compromises, and for me, there are other priorities.
It makes sense at a high level though, like for public APIs. Ideally, I'd rather write both sides at the same time, as to have a real use case rather than just a test, and have both evolve together, but it is not always possible. In that case, writing the test first may be the next best thing.
Re: To be a better programmer, write little proofs in your head
#89Earlier quoted context omitted.
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 t…
It’s a good direction to follow, but it can only get you so far. Some pieces of code do naturally evolve into a functional formalism, while others are inherently imperative. Usually, the top levels of your program (event loop) are imperative and deal with stateful “devices” like IO, the screen and storage subsystems. The “leaf” functions from the call graph can be functional, but you still can’t reason about the whol…
Yes, but if you can actually drive all that out to the very top level and leave everything everything else clean, that’s a huge improvement over how many programs are structured.
Re: To be a better programmer, write little proofs in your head
#90Earlier quoted context omitted.
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 tha…
Interesting, could you show me a formal proof that can't be expressed in logic (ie. code) and then tested? My thought here is that since proofs are logic and so is code you can't have a proof that can't be represented in code. Now admittedly this might look very different than typical say JUnit unit tests but it would still be a test validating logic. I am not saying every system is easily testable or deterministic b…
Tests can generally only test particular inputs and/or particular external states and events. A proof abstracts over all possible inputs, states, and events. It proves that the program does what it is supposed to do regardless of any particular input, state, or events. Tests, on the other hand, usually aren't exhaustive, unless it's something like testing a pure function taking a single 32-bit input, in which case you can actually test its correctness for all 2^32 possible inputs (after you convinced yourself that it's truly a pure function that only depends on its input, which is itself a form of proof). But 99.99% of code that you want to be correct isn’t like that.
As an example, take a sorting procedure that sorts an arbitrarily long list of arbitrarily long strings. You can't establish just through testing that it will produce a correctly sorted output for all possible inputs, because the set of possible inputs is unbounded. An algorithmic proof, on the other hand, can establish that.
That is the crucial difference between reasoning about code versus merely testing code.