Hacker News Reader

Comment by nautilus12 | Hacker News Reader

I havent thought of this before but i was a mathematician that does software engineering, and Im starting to see some stark similarities between a mathematical proof and a "test" as in a unit test. I imagine if you went down this road you would end up with something very similar if not identical to TDD. What i was hoping this thread would discuss is how to turn software design patterns like the adaptor or factory patterns into a science in the same way that differential topology turns differential equations from a haphazard collection of methods into a rigorous science. I dont know why more people havent focused on formulating this more practical side of software engineering. Why is it that SOLID works so well, etc

View on HN

Dijkstra spent a lot of his research effort on ways to prove that programs are correct.

"Today a usual technique is to make a program and then to test it. But: program testing can be a very effective way to show the presence of bugs, but it is hopelessly inadequate for showing their absence. The only effective way to raise the confidence level of a program significantly is to give a convincing proof of its correctness."

https://www.cs.utexas.edu/users/EWD/ewd03xx/EWD340.PDF

"I don't need to waste my time with a computer just because I am a computer scientist." - Dijkstra

This basically describes the dichotomy between CS and software engineering.

There is great wisdom in that observation, but I also enjoyed Knuth's take on the matter:

"Beware of bugs in the above code; I have only proved it correct, not tried it."

http://www-cs-faculty.stanford.edu/~knuth/faq.html

Yes, this is of extreme interest to me as well. The why behind SOLID. I think you could formulate more rigorous support based upon information and graph theory, maybe neuroscience, and other areas I'm less familiar with.

For example, the Single Responsibility Principle (SRP) is primarily concerned with making software more manageable on both an individual and team basis. How? By minimizing:

1. Communication overhead between teams/modules

2. Information overload in an individual

You could look at #1 from a graph-theoretic and information basis. I'm sure there are many interesting things to prove there. Like Amdahl's and the opposite of Metcalfe's Law [1][2] applied to team/communication/module dependencies. Just as a basic example, if one class has 10 responsibilities shared by 10 engineers with no boundaries specified, then the probability of conflict and unintended consequences rises. Thus the rate of development slows.

As for #2, applying more rigor and proof to the question of how these principles help a human understand quicker.

I don't have the necessary background right now to explore this in more detail, but like you, I'm very interested in any possible formulations.

[1]: https://en.wikipedia.org/wiki/Amdahl%27s_law

[2]: https://en.wikipedia.org/wiki/Metcalfe%27s_law

The problem is that even things like "how many people touch this class" and "how many external teams do we work with" aren't simple at all. Some external teams are much easier to work with than others. Sometimes you want your whole team to intimately understand an area of your code. Making software is an intensely human process, which is why managing software teams is almost entirely about considering the people on your team, and what makes each of them different.

Tests are negative proofs; you can show that a specific invocation doesn't fail. But unless they are exhaustive over the input space, they are never positive. You can't say something works universally.

I am not a full subscriber to SOLID. I think it promotes a certain kind of degenerate over-abstraction that leads to bugs of a different nature, premature decisions on what needs future substitution, and decreases agility in the medium term.

Reply on news.ycombinator.com