[xg15]

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.

[Nevermark]

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]

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]

Yeah, and I’m saying if your code is idiomatic you get necessary invariants for free.

[wahern]

I bought The Practice of Programming years ago. It's a great book that is no less relevant today, but I don't see your argument. The suggestions you've summarized are critical advice, but rather than obviate the need for the proof-like mindset, they complement it. Idiomatic code doesn't directly help you solve and implement difficult algorithmic or architectural problems. However, idiomatic code certainly helps reduce noise so that the irreducibly complex aspects of a solution conveniently standout, both conceptually and literally.

[gregorygoc]

I do agree they do complement each other… to some extent. My point was rather that if you write a good code, keeping logical arguments in your head should be reduced to the minimum. To the point that only testing edge cases and a happy path in your mind should be sufficient.

To give a more concrete example: I have recently seen a very complicated piece of logic checking whether a subsequent code should be even invoked, but it was hidden in a debris of core logic and other verification. It easily could have been separated and rewritten as a series of early returns and this is what a precondition is. I’m sure someone who wrote the code had it in their mind but was not familiar enough with the early return technique to embed this in code. Had they been, their brain power could’ve been utilized more efficiently.

[auggierose]

Is idiomatic related to idiotic?

[spauldo]

It is if you're writing vimscript.

[bmn__]

People downvoted you because instead of polluting the discussion, you could have looked this up yourself.

The answer is yes, both words are related to idios, "own", "self", "private".

[auggierose]

Please don't comment about the voting on comments. It never does any good, and it makes boring reading.

https://news.ycombinator.com/newsguidelines.html

[bmn__]

lame

[mprast]

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