111–120 of 181 posts
I'm curious though. When you're coding, do you actually pause and think through the logic first, or is it more like writing and fixing along the way?
One thing that I feel that is discussed less is, what are the high level constraints and levers that can be set to enable a group of programmers to become a better programmers. For example, how much impact does architecture have? bug tracing, choice of language, tools. People handwave and say that one is better than another because of , , but to be able to explain how each of this choice impacts the code in a semi-ri…
Earlier quoted context omitted.
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.
Yeah, and I’m saying if your code is idiomatic you get necessary invariants for free.
Oh, 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…
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.
That they work for binary search is a very strong signal to people not familiar with them that they work for nearly everything (they do).
Earlier quoted context omitted.
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 yo…
I agree with that but I would say that if I required formal verification of that kind I would move the proof based rationale into the type system to provide those checks. I would add Tests can be probabilistically exhaustive (eg property based testing) and answer questions beyond what proof based reasoning can provide ie. is this sorting of arbitrary strings efficient and fast?
Oh, 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?
Earlier quoted context omitted.
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.
Every time I needed to write something algorithmically demanding, I could do it in a day or two. Im not into Leetcoding, or competitive coding.
Most regular everyday programmers can work these things out in one or two workdays.
Its definitely not like the competitive programmers say, like if you aren't into this full time, at the time you need to write something you won't have access to time, internet and even an IDE and have to write the code in a Google doc(which needs internet connection, when I pointed this out in the interviews they didn't like it).
Writing correct proofs is hard. Program verification is hard. In my opinion if you are hand weaving it there’s no benefit. Thinking about invariants and pre-post conditions is often unnecessary or greatly reduced if you write idiomatic code for the language and codebase. Check out “The Practice of Programming” by R. Pike and B. W. Kernighan. The motto is: simplicity, clarity, generality. I find it works really well i…
But writing clean and clear code in the hopes that it's good aesthetics will result in correctness would be cargo culting. (Writing clean code is still worthwhile of course, and clean code + code review is likely to result in better correctness.)
Form follows function, not the other way around.
How to Think About Algorithms by Jeff Edmonds.
Persuasive Programming by Jerud Mead and Anil Shinde.