I really liked this post. Does anyone have other blog posts that they liked that articulates a taste for good engineering?
To be a better programmer, write little proofs in your head
91–100 of 181 posts
Re: To be a better programmer, write little proofs in your head
#92Another thing I learnt from my math degree that I find helps a lot when programming and software engineering more generally is *defining your terms*.
So many communication issues on teams occur when people are using the same words to mean different things.
Re: To be a better programmer, write little proofs in your head
#93One 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-rigorous way by explaining all the way of how it impacts individual code components and their interaction (as a graph or a tree) would be immensely helpful. If anyone knows of resources like that, please let us know
Re: To be a better programmer, write little proofs in your head
#94I’m too old for that, so I write the algorithm on paper and run it with some numbers, also on paper. I don’t have the patience to do it often but whenever I did I usually got it done in one or two tries.
Re: To be a better programmer, write little proofs in your head
#95Oh, 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?
About 100%?
When do you write code that doesn't need to search? (Unless you hand it all to the database, in which case... sure, you're good)
Re: To be a better programmer, write little proofs in your head
#96This is similar to an intuition I've had about what it means to program "algorithmically". We often draw a distinction between "algorithms" and "business logic", but fundamentally they are the same thing. They are both plans of the steps necessary to accomplish a goal. The only difference, in my mind, is the style in which the program is written. To program "algorithmically" means to take steps to make undesirable program states impossible to represent.
- In the case of search or sort algorithms, where the primary concern is the speed of computation, undesirable states would be performing unnecessary or duplicate computations.
- In the case of encryption algorithms, undesirable states would be those that leak encrypted data.
- In the case of an order shipping and fulfillment system, an undesirable state would be marking an order as fulfilled when not all of the items have been delivered.
The more care that is taken to prevent undesirable states, the more the program takes on an algorithmic style. And the only way you can be sure that those undesirable states are impossible is to think in terms of proofs and invariants.
Re: To be a better programmer, write little proofs in your head
#97One 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…
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.
Re: To be a better programmer, write little proofs in your head
#98Real programmers use butterflies.
---
Let me elaborate: there is a huge history of dubious allegations of what constitutes "a real programmer" or stuff that makes you "a better programmer".
Combobulation and descombobulation of McGuffins is often the best analogy though. Not to dismerit other kinds of thinkings, but already dismeriting them, that's what this is all about. When in doubt, showing the code is often what works.
Re: To be a better programmer, write little proofs in your head
#99Another thing I learnt from my math degree that I find helps a lot when programming and software engineering more generally is *defining your terms*. So many communication issues on teams occur when people are using the same words to mean different things.
lookup "ubiquitous language" it's a phrase from domain driven design
Re: To be a better programmer, write little proofs in your head
#100Earlier quoted context omitted.
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…
I would lean towards types and property testing here using tools like Coq.