Specifications: Explain the downsides of formal verification

[amyjko]

Something I felt that the chapter could do better in is giving more evidence for how writing formal specifications has a downside. I felt that this paragraph did give examples and explained some examples well, but unlike the upside of writing formal specifications, there was not as much supporting evidence saying why the downsides were so crucial.

Something I was curious on and wanted more elaboration was the various kinds of barriers that software engineers have when writing formal specifications. There was one point mentioned, which was the difficulty and time to maintain functional specifications. However, I was interested in learning if there were other factors that impacted their commitment to formal specifications, and exactly what the difficult points were when writing them. This would also help me understand what developers prioritize as "worth the effort" for formal specifications versus which ones don't need as much time spent on them.

In this chapter, the author discussed the different aspects of writing a formal specification. In some cases like life or death, money-related area, formal specifications are important and 100% worth the effort. But the downside to writing a formal specification when software failure isn’t high is that it can deter developers to use overly deductive methods. Though, in this chapter, I wished the author went more in-depth about how-to-write formal specifications like the details that developers need to include or how we can go about writing a simple and concise specification.

One thing I want to learn about more is how formal specifications can have downsides. The article says that “When the consequences of software failure aren’t so high, the difficulty and time required to write and maintain functional specifications may not be worth the effort”, deterring coders from focusing on failure prevention (Ko). It also mentions how it can be easy to mix up proper typing for input values. But since all of this was limited to a  single paragraph, are there any other important downsides that formal specifications have on development that we should know? I’m definitely interested in knowing if there are common mistakes or conventions that people make while writing formal specifications that may (for example) be convenient to use until there is a disruption or failure in the program. Or are there other downsides to writing specifications that causes developers to avoid writing them? I feel that the more I know about the reasons why people tend to avoid these issues, the more ways I can think of how to tackle these challenges.

To start off, I am just curious how the name "cowboy coding" came to be because I went onto the wiki page but it did not tell me.

In the reading, it mentions how there are tradeoffs with writing formal specifications and that companies only make you write it if they have to be completely unambiguous. And then it says that when software failure isn't so high, then formal specifications are not worth the effort. I was just curious how common it is in companies for them to not write formal specifications. It feels like most companies would want their developers to write formal specifications even if their work is not completely unambiguous.