Friday, July 17, 2015

Programming by Thinking

In my second post (Programmers as Children) I complained about the fact that programmers work with their fingers instead of using their brains.  This is gradually getting worse instead of better, with growing academic research concentrating on the use of examples from the internet, search tools to find such examples for specific questions, and so on.  Of course, there are many websites containing advice for various programming domains, and the examples they provide are often quite useful.  However, copying these into your own code without understanding what they do, and what are the wider implications (for example, on performance and security), is a recipe for disaster.

The April 2015 issue of Communications of the ACM contains several articles that should be required reading for every software developer.  The first is Leslie Lamport's viewpoint article, "Who Builds a House without Drawing Blueprints."  No engineering discipline proceeds to build anything without first analyzing the requirements, making initial designs and analyzing them from various points of view (such as cost, safety, standards, and legal implications) -- in other words, thinking deeply about the problem and possible solutions.  But in the (arguably misnamed) discipline of software engineering, starting with coding is all too often the norm, and is even praised as a methodology.  (I am not implying that any of the agile methodologies advocates that; quite the contrary!  However, agile methods are often misunderstood as "don't think before you code.")

Lamport argues that thinking is necessary before coding, and that writing specifications is an excellent way to focus your thinking.  The specifications need not always be formal, although Lamport makes a good case for using formal specifications, and using tools to check them.  Specifically, TLA+ is a formal specification language created and used by Lamport himself in various projects.

You may be inclined to dismiss this as only academic, and, unfortunately, this is the too-prevalent view.  However, you may learn otherwise if you read another article in the same issue, "How Amazon Web Services Uses Formal Methods."  This article describes how TLA+ was used in several critical Amazon projects, and discovered bugs that the authors admit they could not have found otherwise.  In some cases, Amazon engineers used TLA+ successfully on their projects after two weeks of self-learning.

Of course, getting the specifications right does not mean that the code will be correct as well.  Tool support for verifying the code against its specification would be very helpful, and this is an area of active research.  However, not getting the specifications right is almost a guarantee that the code will have bugs.  This is particularly true for large concurrent systems, which are a source of extremely subtle bugs that programmers have great difficulties understanding and predicting.

And while you have the April issue in your hands, I recommend you also read the article "Security Challenges for Medical Devices."  It discusses safety, security,  and privacy issues with various kinds of medical devices.  Even hospital information systems have such issues, but they are most critical with implanted devices such as pacemakers.  Modern implantable devices communicate wirelessly to provide information they collect, and sometimes they can even be programmed wirelessly.  This creates health hazards from mistakes but also deliberate attacks.  Even devices that only provide information are dangerous if this information is modified anywhere along the way from the device to the physician (including in IT systems that store or transmit this information), since this could lead to the wrong treatment being applied.

Security cannot be added as an afterthought; it must be designed-in from the beginning.  While not all systems have the same security implications as medical devices, the whole chain is as strong as the weakest link, which implies that security is crucial to more systems than would be immediately obvious.  This helps drive home Lamport's point.  Think before you code!

#formalmethods #specifications