Drawing a picture is a perfectly valid and legitimate start. However I think there are many problems where a picture is not sufficient and it's necessary to have good, reliable mathematics to sketch out our designs and prove properties of them.
A sketch is still useful the the absence of nothing else. But we don't build bridges and skyscrapers that way so why is it good enough for our data-centres and applications?
I don't think lives have to be on the line in order for software to be considered harmful if not built correctly. There are plenty of problems where having a thoroughly checked design will save you plenty of headaches and afford you many more opportunities.
> However I think there are many problems where a picture is not sufficient and it's necessary to have good, reliable mathematics to sketch out our designs and prove properties of them.
It's necessary to have a formal language to describe this design. Such a formal language needs to have one and only one interpretation. We should be able to take a document written with that formal language and verify that it meets our assumptions. We should also be able to verify that the final implementation is isomorphic to the design.
Luckily such tools are ubiquitous. You can use whatever programming language you like to specify your design. In the case where the programming language is defined poorly, then you must also decide what build system and run time environments you will support ahead of time.
You can document your assumptions using the same programming language. This is made easier if you use a "test framework", but if needed you can also roll your own. You can validate your design by running the tests against your design. Normally it is best to break up your design into "units" that make it more clear how to validate your assumptions. You can then add some extra validation that the composition of "units" transitively validates your assumptions.
You can verify that your final produce adheres to that design because there will be a 1:1 mapping from the design to the final product (i.e. the final product will be implemented using the same code as your design). There are wonderful tools that will tell you the "coverage" of code used in the final product that has been validated against the assumptions.
Finally, you can even specify your requirements using the same formal language and verify that the design meets the requirements. Normally you do this by validating that the "integration" of "units" meets your assumptions. This should not be done without individually validating the assumptions on the "units", though, because the "integration" can lead to exponentially growing alternatives. Normally it is infeasible to validate each alternative.
Yes, this reply is tongue in cheek, but I am not ignorant of formal specification methods. They have their place. That place is currently not in a professional software development shop. We have better methods at the moment. Possibly formal specifications methods will improve to the point where we can reasonably use them, but we aren't there yet.
> Possibly formal specifications methods will improve to the point where we can reasonably use them, but we aren't there yet.
I disagree. Amazon has had great success employing TLA+ in finding bugs, testing design changes, and chasing aggressive optimizations [0].
Perhaps it is because there are myths that are still floating around regarding formal methods that still make developers cringe when they hear mention of them [1].
None the less I couldn't find reference to it in the book... did I miss it?
And besides... unit tests, I'm sure you are aware, aren't good enough alone. They can only increase your confidence in an implementation but they prove nothing.
If we want to start calling ourselves engineers I think we better start looking to how the other engineering disciplines operate. I don't think it will be long before an insurance company comes along and finds actuaries capable of monitoring risk in software development projects and liability becomes a necessary concern.
I had to think about if for a bit, but you are right. My statement was waaay too general. Especially for communication protocols formal specifications are useful now. I still think we have a long way to go before we will be using tools like this every day. The main issue is whether or not it is easier to reason about the correctness of something by inspecting its design or its implementation. We can never prove that the design is correct, only that it is isomorphic to the requirements and the implementation. If there is only one document, the implementation, then the proof of isomorphism is trivial. That was my point. I personally believe that for user facing behaviour is easier and clearer to express with with tests (either integration or unit) and I really don't expect that to change in the near future.
Anyway, I regret the tone of my previous message, which mostly made me look foolish, and thank you for your kind response.
I look for the critical bottlenecks in the application where the cost of failure or mistakes is fairly high. This is where I feel I will get the most "bang for the buck" so to speak.
You don't have to specify the entire application to get the benefit of high level specifications. Even specifying the protocol between two communicating channels can bring benefits.
There's literally millions in commercial and academic activity around it. Maybe tens of millions. It's not dead yet despite me wishing it never had life to begin with haha.
I've seen plenty more work on UML as academics & commercial vendors are still all over it. I couldn't find an example for "Processing" because they picked the stupidest name possible: a word so overused I'm getting results from the food industry, compilers, IRS, and computers all at once.
UML specs them at an abstract level. You build them in code or HDL's. Few, formal methods can do both. Generally, you prove properties in the abstract in one and correspondence with the other. Code-level proofs only came online only in past 5-10 years or so in a subfield 40 years old.
So, UML would let you specify data and behavior then confirm properties about them, catch inconsistencies in requirements, or aid integrations. SysML is used for this in industry with verification results in academia even for UML as I showed. So, it's reality rather than theory even if you or I think better methods exist. I'll take a combo of Z, B, CSP, and/or Statecharts over UML anyday. Coq and HOL if I was specialist enough.
Not saying you're wrong: At the end of the day to the degree that any of these methods (UML, TLA+, whatever) formally prove correctness is the same degree that they gain the features of a turing-complete programming language. Which comes back to the notion design is the source code itself and represents the majority of the work. The compiler or interpreter is the "construction" phase of the project.
I just took a short look at TLA+ and read a tutorial.
Don't think I could use it without drawing a picture.