[HN Gopher] To be a better programmer, write little proofs in yo...
___________________________________________________________________
To be a better programmer, write little proofs in your head
Author : mprast
Score : 182 points
Date : 2025-07-15 17:05 UTC (5 hours ago)
(HTM) web link (the-nerve-blog.ghost.io)
(TXT) w3m dump (the-nerve-blog.ghost.io)
| hiAndrewQuinn wrote:
| 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 Programming Pearls, gave the task of
| writing an ordinary binary search to a group of professional
| programmers at IBM, and found that _90%_ of their implementations
| contained bugs. The most common one seems to have been
| accidentally running into an infinite loop. To be fair, this was
| back in the day when integer overflows had to be explicitly
| guarded against - but even then, it 's a surprising number.
|
| [1]: https://hiandrewquinn.github.io/til-site/posts/binary-
| search...
| qsort wrote:
| 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.
| fragmede wrote:
| 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...
| hiAndrewQuinn wrote:
| The bug in that paper is actually the very buffer overflow
| bug I was referring to. Given that Jon himself made that
| error in the "definitive" implementation, it seems unlikely
| that he would have spotted it in the 10% of implementations
| he considered correct. Under Google's stricter criteria it
| seems likely to me that not a single person got the search
| implementation truly correct enough.
| sedatk wrote:
| 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.
| None4U wrote:
| 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?
| JohnKemeny wrote:
| 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.
| monkeyelite wrote:
| 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.
| Animats wrote:
| Now if we can get LLMs to do that, they might code better. Proofs
| are a lot of work, but might keep LLMs on track.
| mprast wrote:
| I was thinking the same thing!
| Nevermark wrote:
| In any other industry the "worker class" would be sabotaging
| the machines.
|
| In the merry software world, the challenges of improving our
| potential replacements are far too interesting and satisfying
| to leave room for any worry about consequences! :)
| bcheung wrote:
| The problem is the training corpus tends towards mediocre code.
| But with an agentic loop that analyzes the code against those
| criteria and suggests changes then I think it might be
| possible. I wouldn't try to get it to generate that right off
| the bat.
| AIPedant wrote:
| Most proof assistants do a good job with autogenerating a
| (deterministically correct) proof given a careful description
| of the theorem. Working on integrating this into mainstream
| languages seems much more worthwhile than training an LLM to
| output maybe-correct proof-seeming bits of text.
| gregorygoc wrote:
| 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 in a
| day job.
|
| On a slightly related note... Competitive programming is
| surprisingly good at teaching you the right set of techniques to
| make sure your code is correct. You won't progress beyond certain
| stage unless you pick them up.
| wizzwizz4 wrote:
| 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.
| gregorygoc wrote:
| No, appropriate abstractions are insufficient for my
| argument. For example: there's one way to write an idiomatic
| loop in C and it inherits necessary invariants by
| construction.
|
| I highly recommend reading the book, it explains concept of
| writing idiomatic code way better than I ever could.
| chowells wrote:
| That's a really funny example, given how many bugs have
| been found in C programs because idiomatic loops are wrong
| in the edge cases.
|
| How do you idiomatically write a loop to iterate over
| signed ints from i to j (inclusive) in increasing order,
| given i <= j?
|
| What does that loop do when j is INT_MAX?
| wk_end wrote:
| I can imagine someone who sketches out little proofs in
| their head - or even on paper - missing that case too.
| It's easy to forget you're not doing normal arithmetic
| when doing arithmetic in C!
| chowells wrote:
| Yeah, it's a hard case in general. But C's idioms really
| don't encourage you to think about it. You really need to
| default to a loop structure that checks the termination
| condition after the loop body but before the increment
| operation for inclusive end coordinates.
|
| It's easy to think that's what do/while is for, but it
| turns out to be really hard to do the increment operation
| after the conditional, in general. What you really want
| is a loop structure with the conditional in the middle,
| and the only general purpose tool you get for that is a
| break. C (or any language with similar syntax) really
| doesn't have an idiom for doing this correctly.
| xg15 wrote:
| 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.
| mprast wrote:
| yes, what i had in mind were more proof sketches than proofs
| Nevermark wrote:
| Yes, we could call this "maintaining plausible provability".
|
| Code for which there is not even a toehold for an imagined
| proof might be worth cordoning off from better code.
| Sharlin wrote:
| Types constitute this sort of a partial proof. Not enough to
| encode proofs of most runtime invariants (outside powerful
| dependent type systems) but the subset that they _can_ encode
| is extremely useful.
| gregorygoc wrote:
| Yeah, and I'm saying if your code is idiomatic you get
| necessary invariants for free.
| auggierose wrote:
| Is idiomatic related to idiotic?
| pipes wrote:
| Could you elaborate on those techniques from competitive
| programming please. Genuinely interested! :)
| mathgradthrow wrote:
| 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.
| monkeyelite wrote:
| 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.
| bluetomcat wrote:
| > My thesis so far is something like "you should try to write
| little proofs in your head about your code." But there's actually
| a secret dual version of this post, which says "you should try to
| write your code in a form that's easy to write little proofs
| about."
|
| Easier said than done. It is certainly feasible on greenfield
| projects where all the code is written by you (recently), and you
| have a complete mental model of the data layout and code
| dependencies. 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.
| akavi wrote:
| 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)
| mprast wrote:
| yeah, this is what i was trying to get at with that notion of
| "proof-affinity"; imo a well-structured codebase is one in
| which you can easily prove stuff to yourself about code you
| didn't necessarily write
| xg15 wrote:
| 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.
| msteffen wrote:
| 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.
| bluetomcat wrote:
| 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 whole program when it is imperative at the top.
| thfuran wrote:
| 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.
| jimbokun wrote:
| > 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".
| hinkley wrote:
| I just finished cave diving in a code base that's had a very
| old ticket to clean up the mess.
|
| I went in with 3 tickets in mind to fix. I found half a dozen
| more while I was down there, and created 2 myself. I don't
| know if I got off easy or I was distracted and missed things.
|
| The other project I'm working on is not dissimilar. Hey did
| you guys know you have a massive memory leak?
| monocasa wrote:
| And in fact, when you look at formally proven code, 80% of
| the shtick is reducing complexity of mutation to something
| tractable. That's valuable whether or not you then actually
| go through the process of formally proving it.
| hinkley wrote:
| > 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.
| nayuki wrote:
| I learned the foundations of theoretical computer science in
| university. I agree with the sentiment of this post, though it is
| hard to perform in practice.
|
| In addition to pre-conditions and post-conditions, I would like
| to emphasize that loop invariants and structural induction are
| powerful techniques in CS proofs.
| https://en.wikipedia.org/wiki/Loop_invariant ,
| https://en.wikipedia.org/wiki/Structural_induction
|
| These notes from UofT's CSC236H are on-topic:
| https://www.cs.toronto.edu/~david/course-notes/csc236.pdf#pa...
| sitkack wrote:
| Those notes are great, David Liu seems while a wholesome dude
| https://www.cs.toronto.edu/~david/research.html
| skybrian wrote:
| The software he's working on seems rather obscure and perhaps not
| launched yet? get-nerve.com can't be resolved.
| mprast wrote:
| not launched yet! I will put up a post when it launches; coming
| in a few months!
| roadside_picnic wrote:
| What's interesting about this view is that theorem provers
| ultimately boil down to sufficiently advanced type checking (the
| book _Type Theory and Formal Proof_ is an excellent overview of
| this topic). Literally the heart of proof assistants like Lean is
| "if it compiles, you've proved it".
|
| So more practical type systems can be viewed as "little" theorem
| provers in the sense the author is describing. "Thinking in
| types" so to speak, is mathematically equivalent to "writing
| little proofs in your head". I would also add that _merely_ using
| types is not equivalent to "thinking in types" as one would be
| required to do writing a sufficiently advanced Haskell program.
| trealira wrote:
| It's true that theorem provers can be just sufficiently
| advanced type systems (the Curry Howard correspondence), but
| not all theorem provers operate that way. Isabelle/HOL operates
| on higher order logic. Imperative ones like SPARK or Dafny just
| rely on encoding preconditions and postconditions and things
| like loop invariants and just use SMT solvers for verification,
| IIRC.
|
| Having an advanced type system does seem to encourage this sort
| of informal proof oriented thinking more than imperative and
| somewhat typeless languages do, though, since preconditions and
| postconditions and loop invariants and inductive proofs on
| loops are things you have to do yourself entirely in your head.
| xg15 wrote:
| I'd also add mutability and immutability to the list of
| properties. Keeping as much state as possible immutable doesn't
| just help with multithreading, it will also greatly reduce the
| headache when trying to understand the possible states of a
| program.
| jimbokun wrote:
| The article does include those.
| dblohm7 wrote:
| I don't do this often, but when I do, it's almost always when
| writing non-trivial concurrent code. I'll often "fuzz" the
| scheduling of multiple tasks around the region of code I'm
| working on to prove to myself that it works.
| cespare wrote:
| I really identify with this way of thinking. One domain where it
| is especially helpful is writing concurrent code. For example, if
| you have a data structure that uses a mutex, what are the
| invariants that you are preserving across the critical sections?
| Or when you're writing a lock-free algorithm, where a proof seems
| nearly required to have any hope of being correct.
| taeric wrote:
| I feel like this is reaching for the vocabulary that you get in
| mathematics of axioms, postulates, and theorems. Not in a bad
| way, mind. Just the general idea of building a separate
| vocabulary for the different aspects of a system of knowledge.
|
| I also think things get complicated with holding things constant
| as a necessity. Often times, the best way to find a bug is to ask
| not "how was this possible?" but "why would another part of the
| system modify this data?"
|
| Obviously, if you can make things reference capable data, you
| should do so. But, all too often "this data being X" has a
| somewhat self evident explanation that can help. And just "copy
| so I don't have to worry about it" lands you squarely in "why is
| my copy out of date?"
| phkahler wrote:
| Another nice pattern is to have any particular value written
| exactly once, or from exactly one place in the code if it gets
| updated.
|
| For embedded control I'm finding the blackboard pattern with
| single assignment to be super useful.
| bcheung wrote:
| I wonder how many of these rules can be incorporated into a
| linter or be evaluated by an LLM in an agentic feedback loop. It
| would be nice to encourage code to be more like this.
|
| I notice you didn't really talk much about types. When I think of
| proofs in code my mind goes straight to types because they
| literally are proofs. Richer typed languages move even more in
| that direction.
|
| One caveat I would add is it is not always desirable to be forced
| to think through every little scenario and detail. Sometimes it's
| better to ship faster than write 100% sound code.
|
| And as an industry, as much as I hate it, the preference is for
| languages and code that is extremely imperative and brittle. Very
| few companies want to be writing code in Idris or Haskell on a
| daily basis.
| ngruhn wrote:
| Sorry for being pedantic but isn't the story that
| types=theorems and programs=proofs?
| sitkack wrote:
| "Propositions as Types" by Philip Wadler
| https://www.youtube.com/watch?v=IOiZatlZtGU
| GMoromisato wrote:
| Totally tangential, but I love to read post-mortems of people
| fixing bugs. What were the initial symptoms? What was your first
| theory? How did you test it? What was the resolution? Raymond
| Chen does this a lot and I've always enjoyed it.
|
| I learn more from these concrete case studies than from general
| principles (though I agree those are important too).
|
| One of my most recent bugs was a crash bug in a thread-pool that
| used garbage-collected objects (this is in C++) to manage network
| connections. Sometimes, during marking, one of the objects I was
| trying to mark would be already freed, and we crashed.
|
| My first thought was that this was a concurrency problem. We're
| supposed to stop all threads (stop the world) during marking, but
| what if a thread was not stopped? Or what if we got an event on
| an IO completion port somehow during marking?
|
| I was sure that it had to be a concurrency problem because (a) it
| was intermittent and (b) it frequently happened after a
| connection was closed. Maybe an object was getting deleted during
| marking?
|
| The only thing that was weird was that the bug didn't happen
| under stress (I tried stress testing the system, but couldn't
| reproduce it). In fact, it seemed to happen most often at
| startup, when there weren't too many connections or threads
| running.
|
| Eventually I proved to myself that all threads were paused
| properly during marking. And with sufficient logging, I proved
| that an object was not being deleted during marking, but the
| marking thread crashed anyway.
|
| [Quick aside: I tried to get ChatGPT to help--o3 pro--and it kept
| on suggesting a concurrency problem. I could never really
| convince it that all threads were stopped. It always insisted on
| adding a lock around marking to protect it against other
| threads.]
|
| The one thing I didn't consider was that maybe an object was not
| getting marked properly and was getting deleted even though it
| was still in use. I didn't consider it because the crash was in
| the marking code! Clearly we're marking objects!
|
| But of course, that was the bug. Looking at the code I saw that
| an object was marked by a connection but not by the listener it
| belonged to. That meant that, as long as there was a connection
| active, everything worked fine. But if ever there were no
| connections active, and if we waited a sufficient amount of time,
| the object would get deleted by GC because the listener had
| forgotten to mark it.
|
| Then a connection would use this stale object and on the next
| marking pass, it would crash.
| pokemyiout wrote:
| Is there a typo in the induction section? Should `simplifyTree`
| and `simplifyGraph` be the same function?
|
| function simplifyTree(root: Node): Node { let
| newChildren = [] as Array<Node>; for (const child of
| root.children) { const simplifiedChild =
| simplifyGraph(child); if
| (shouldContract(simplifiedChild)) { for (const
| grandChild of simplifiedChild.children) {
| newChildren.push(grandChild); } } else {
| newChildren.push(simplifiedChild); } }
| root.children = newChildren; return root; }
| dkenyser wrote:
| This reminds me of reading Accelerated C++ back in the day and I
| think the part that stuck with me most from that book was the
| idea of "holding the invariant in your head" (I'm paraphrasing a
| bit).
|
| It made me think a lot more about every line of code I wrote and
| definitely helped me become a better programmer.
| ryandv wrote:
| Hah, nonsense. All of this academic computer science is like the
| rest of higher mathematics - utterly useless. Hoare triples?
| Induction? Proof? Knowledge of such esoterica is soon to become
| obsolete, since all this learning is already baked into a large
| language model that can apply this theory on your behalf, at
| 1000x the speed. Why bother thinking through things with your
| antiquated neural wetware when the computer can do it better,
| faster, and more correctly?
|
| Developers who still "think through problems" instead of just
| managing agents to solve problems on their behalf will be
| obsoleted in the next 2 years.
| Culonavirus wrote:
| We're so fucked.
| mathgradthrow wrote:
| Monotone just means order preserving. f is monotone if f(a) >=
| f(b) whenever a >= b.
| wrs wrote:
| As an undergrad at Carnegie Mellon in the 80s, I was explicitly
| _taught_ to do all of these things in one of the first-year
| programming courses. And it has served me very well since then.
|
| I especially remember how learning the equivalence of recursion
| and induction immediately eliminated the "frustrated trial and
| error" approach for making recursive algorithms that work.
| TheShermanTank wrote:
| Took the course last year, and I started to appreciate it more
| while taking functional programming lmao
| wiseowise wrote:
| To be a better programmer, program more and read less bullshit on
| the internet.
| tristramb wrote:
| The idea that you should design programs with proof in mind goes
| back to T. J. Dekker's solution to the mutual exclusion problem
| in 1959. The story is told by Edgser Dijkstra in EWD1303 (https:/
| /www.cs.utexas.edu/~EWD/transcriptions/EWD13xx/EWD130...). Much
| of Dijkstra's later work can be seen as him working out the
| consequences of this insight.
| thesuperbigfrog wrote:
| Why not include little proofs in the code when you can?
|
| Several programming languages and libraries support Design-by-
| Contract (https://en.wikipedia.org/wiki/Design_by_contract) which
| lets you specify preconditions, postconditions, and invariants
| directly in your code.
|
| Those predicates can be checked in various ways (depending on how
| deeply Design-by-Contract is supported) to help you know that
| your code is working correctly.
|
| Ada supports Design-by-Contract as part of the language:
| https://learn.adacore.com/courses/intro-to-ada/chapters/cont...
|
| SPARK extends Ada Design-by-Contract into full proofs:
| https://learn.adacore.com/courses/intro-to-spark/index.html
|
| Rust has the Contracts crate:
| https://docs.rs/contracts/latest/contracts/
|
| Other programming languages have various levels of support or
| libraries for Design-by-Contract:
| https://en.wikipedia.org/wiki/Design_by_contract#Language_su...
| bigmadshoe wrote:
| Even standard assertions work as a version of this
| thesuperbigfrog wrote:
| Standard assertions certainly are better than keeping the
| little proofs only in your head.
|
| Many Design-by-Contract implementations are nicer than
| standard assertions because they help to express intent
| better and easily refer to the 'old' value of a parameter to
| verify desired results.
| bubblebeard wrote:
| This is something I've practiced myself quite a lot in recent
| years, and in my experience it's so much harder while at your
| desk. Doing something else while letting your brain work really
| helps. For me, that's usually going for a walk, taking a run in
| the woods, or doing some repeditive household chore.
| JohnMakin wrote:
| I think I stumbled across a similar concept in the more difficult
| post-grad classes I ended up in a long time ago. I began at some
| point late in my undergrad doing math tests entirely in pen. I
| didn't understand why, but it resulted in higher scores almost
| always, and much neater scratchwork, which I had attributed to
| the reason, but I think what was helping was something along the
| lines of what this post is getting at.
|
| What was helping me was that before I wrote a single expression,
| I thought about it carefully in my head and where it would lead
| before putting pen to paper, because I didn't want to make a
| bunch of messy scratch out marks on it. Or, sometimes, I'd use a
| healthy amount of throwaway scratch paper if allowed. Once my
| path was fully formed in my head I'd begin writing, and it
| resulted in far fewer mistakes.
|
| I don't always take this approach to writing code but often I do
| formulate a pretty clear picture in my head of how it is going to
| look and how I know it will work before I start.
| ge96 wrote:
| While having been employed as a developer for almost 7 years now,
| I remember taking this class maybe discrete math, I was not a fan
| of that class, where you have problems like p -> q
|
| Also farthest in math/physics I got was intro to quantum
| mechanics which the multiple-pages to solve a problem lost me
|
| Being a good programmer... I don't have a degree so I've never
| really tried to get into FAANG. I also am aware after trying
| Leetcode, I'm not an algorithm person.
|
| What's funny is at my current job which it's a multi-national
| huge entity thing but I have to try and push people to do code
| reviews or fix small errors that make something look bad (like a
| button being shorter than an input next to it).
|
| I am self-aware with true skill, I can make things, but I don't
| think I'd ever be a John Carmack. If you follow a framework's
| pattern are you a good developer? I can see tangible metrics like
| performance/some slow thing, someone better makes it faster.
|
| Recently someone forked a repo of a hardware project I made. It's
| fun watching them change it, to understand what I wrote and then
| change it to fit their needs.
|
| When I see my old code I do recognize how it was verbose/could be
| much simpler.
| pclowes wrote:
| The 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 fail before writing code, write the smallest
| amount of code possible to make the test pass. Repeat.
|
| The next level is how cohesive or tightly coupled your tests are.
| Being able to make changes with minimal test breakage "blast
| radius" increases my confidence of a design.
| swat535 wrote:
| 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.
| pclowes wrote:
| I agree on the Dogma aspect. Plenty of times I have abandoned
| it. However, I did find it very helpful to spend my first
| couple years in a strict Xtreme Programming (XP) shop. The
| rigor early on was very beneficial and its a safety net for
| when I feel out of my depth in an area.
|
| I tend to go the other way, I don't use TDD when I am playing
| around/exploring as much as when I am more confident in the
| direction I want to go.
|
| Leaving a failing test at the end of the day as a breadcrumb
| for me to get started on in the morning has been a favored
| practice of mine. Really helps get the engine running and
| back into flow state first thing.
|
| The dopamine loop of Red -> Green -> Refactor also helps
| break through slumps in otherwise tedious features.
| saurik wrote:
| 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.
| pclowes wrote:
| 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 but overall, all else equal, the more tested
| and testable a system is the better it is.
|
| IME things that are very hard to test are often just poorly
| designed.
| aljgz wrote:
| 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.
| Kambing wrote:
| > 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.
| JohnKemeny wrote:
| That is stretching the definitions of proofs.
| assert random() != 0.
|
| QED
| GuB-42 wrote:
| 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.
| JohnKemeny wrote:
| 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.
| GuB-42 wrote:
| > 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.
| init1 wrote:
| Instead of just thinking about the proof in your mind or putting
| it in comments you can actually embed pre/post conditions and
| compile time proofs in actual code using ADA SPARK. You use Pre
| and Post aspects for subprograms and pragma Invariant for loops
| and such constructs. The spark toolchain will run provers against
| your code and show if it can show the proofs hold.
|
| https://www.youtube.com/watch?v=tYAod_61ZuQ
| linguistbreaker wrote:
| I wonder if there is a rigorous/formal method to identify
| 'monotonicity' in code? Seems like it should be
| straightforward...
___________________________________________________________________
(page generated 2025-07-15 23:00 UTC)