The steep learning curve for these languages is a barrier to entry for many people. Part of the reward for this effort is an associated mystique about having mastered the special knowledge.
As computation has become pervasive, more and more people who are not professionally trained as programmers are creating and tailoring software as a means to achieve goals of their own. These vernacular software developers are principally interested in their own tasks, not in the software as a primary objective.
Many vernacular software developers are highly trained in their own domains and only lightly trained in traditional programming. They use a variety of tools and notations including spreadsheets, scripting, data schemas, markups, domain-specific languages, visual web development tools, and scientific libraries.
Without adequate specifications for the components, there’s no way to reason formally about the result. When owners of components can change them without notice, users have no assurances. As a result, formal verification is, on the whole, a minor player for real software.
I think the above should be read in parallel with this chapter from Edwin Brady, explaining what type-driven development is all about. :
In other words, there are misconceptions as to what formal verification is. There are many types of formal verification. And it seems that Mary Shaw picked a specific one.
Type-driven development is in active research with many problems still to be solved.
I agree there are various misconceptions, and indeed there are many kinds of formal verification… but I don’t think Shaw is really singling out a specific approach. Perhaps I’ve simplified too much through the tiny quote I selected above, so I’d suggest reading more of the paper itself if you haven’t already.
The overall context of the paper is programming in the world at large, often by domain experts in some area other than programming (Shaw calls them “vernacular software developers”). Many software systems have changing, evolving goals that are difficult, hard, or cost prohibitive to formally specify.
I’ve read parts of Brady’s book, and I’ve tried to use Idris a bit as well, but I ended up developing an impression that for many systems, dependent types are too rigid: a small change to your goals can imply a large reworking of the type structure and overall codebase. It may be a good approach for cases where the requirements and design are fairly clear from the start, but that doesn’t really match my own interests, so it feels like a lot of energy would be lost “gardening types”.
Indeed, and perhaps the “human energy required” to apply tools like this will improve with further innovations.
I think there’s value in starting a separate thread (since it’s not really specific to this paper) about the interplay of types and malleability. It’s a complex topic with many tradeoffs both for and against various kinds of type systems.
Types are a guide for the programmer that alleviates the burden of having to maintain the conceptual model of what they are doing in their head, instead it is made explicit.
It can and should be exploratory, trying new types and new formalisms. But we need to learn how to program in this way.
Edwin’s book gives a good explanation of what we really try to achieve.
It is true though that at this stage, it is difficult to use them. There is a lot of progress that needs to be made.