Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

the-nerve-blog.ghost.io

Post reply on HN
Print view View original

101–110 of 181 posts

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

#101

Post by pclowes »

layer8 wrote: post #90
pclowes wrote: post #77

Earlier 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…

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?

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

#102

Post by kevinventullo »

pipes wrote: post #11
gregorygoc wrote: post #4

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…

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

+1 This is definitely the wall I hit with competitive programming. I logically know how to solve the problem, my code just ends up having one too many bugs that I can’t track down before time is up.

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

#103

Post by pclowes »

GuB-42 wrote: post #79
pclowes wrote: post #66

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 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…

The flow here for me is if the code is doing the wrong thing I:

- Write a test that demonstrates that it is doing the wrong thing

- Watch it fail

- Change the code to do the right thing

- Ensure the test passes

And in return I get regression prevention and verified documentation (the hopefully well structured and descriptive test class) for almost free.

I don't think any amount of testing absolves the programmer from writing clear, intention-revealing code that is correct. TDD is just a tool that helps ensure the programmers understanding of the code evolves with code. There have been so many times where I write code and expect a test to fail/pass and it doesn't. This detects subtle minute drift in understanding.

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

#104

Post by wizzwizz4 »

chowells wrote: post #69
wk_end wrote: post #56

Earlier quoted context omitted.

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!

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…

This may be hubris, but…

  int i = start;
  do thing_with(i) while (i++

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

#105

Post by skydhash »

wanderingmind wrote: post #93

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…

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.

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

#106

Post by mreid »

segmondy wrote: post #99
mreid wrote: post #92

Another 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

Thanks, I hadn't seen that term before.

Just to be clear, I wasn't claiming that "communicating clearly" is a new idea in software engineering, I'm mainly commenting on how effective embracing it can be.

When doing math, pretty much every term is "load-bearing" in that arguments will make use of specific aspects of a concept and how it relates to other concepts.

If you look at most graduate-level math textbooks or papers, they typically start with a whole bunch of numbered definitions that reference each other, followed by some simple lemmas or propositions that establish simple relationships between them before diving into more complex theorems and proofs.

The best software projects I've seen follow a roughly similar pattern: there are several "core" functions or libraries with a streamlined API, good docs, and solid testing; on top of that there are more complex processes that treat these as black-boxes and can rely on their behavior being well-defined and consistent.

Probably the common thread between math and programming is both lean heavily on abstraction as a core principle.

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

#108

Post by chowells »

wizzwizz4 wrote: post #104
chowells wrote: post #69

Earlier quoted context omitted.

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…

This may be hubris, but… int i = start; do thing_with(i) while (i++

I did consider that, but I wrote "in general" for a reason. It works very specifically in the case of "add one" or "subtract one", but it doesn't work with anything more complicated, like chasing pointers or adding/subtracting more than one at a time.

You could write functions to do the update and return the old value so you could use them in the same way, but I don't like this either. This is mostly because it orders the termination check and the update logic the wrong way around. If there's IO involved in checking for the next thing, for example, side effects of that unnecessary operation might interfere with other code.

You could resolve that by moving the termination check into the update logic as well, but now you're seriously complecting what should be independent operations. I don't think the tradeoff is there versus just using a break. But mostly, this is a self-inflicted problem in C's language constructs and idioms. I just don't have this problem in many other languages, because they provide end-inclusive looping constructs.

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

#109

Post by smohare »

mprast wrote: post #17
xg15 wrote: post #8

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.

yes, what i had in mind were more proof sketches than proofs

[dead]

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

#110

Post by [deleted] »

groby_b wrote: post #95
None4U wrote: post #70

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?

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)

[deleted]
Post reply on HN