Formal methods and dependant types are a trap

A response to the previous section might be that there doesn't have to be a distinction between formal methods/proofs, or writing a lot of code at the type level, and writing code that gets shit done. After all, there are things like Algebra Driven Design, where you specify your data types and function signatures to such an minute degree of detail that you can sort of derive the actual program by rote from your types.

The problem with this approach is that is that it doesn't actually solve the problem. Yes, you've essentially turned types into behavior, but in the process you've had to specify your types at such a greater degree of detail and complexity, with so much specific behavior encoded into them, that you've turned your types into code and just pushed the problem back another step.

Think about it: code itself is merely a "specification" of the behavior you want out of your computer. No matter what kind of unexpected bug you have in your code, it's ultimately a problem of your code, as a specification, not being what you imagined it was – incomplete or self-contradictory in some way you missed when you wrote it, not because the computer is mysteriously "disobeying your orders" or something. As we all know, it always does exactly what you tell it to. So code is a formal specification of behavior. Code is just a specification that needs to be fractal in its complexity in order to encompass and contain every behavior needed and every edge case possible, because it is designed to be run on things that are, quite literally, as stupid as rocks.

So the only reason that types and specifications help is that they merely allow you to express a specification for behavior at a higher level of abstraction than your code specifies that behavior – it lets you put things in simpler general terms as a set of declarative constraints. But abstraction is not actually necessarily more amenable to human reasoning at all than particularity: abstraction is actually much harder for humans to reason about. It's just that abstraction lets you compress things so that you can fit more in your memory and get thereby a higher overview of things, whereas a lower level of abstraction is often much easier to reason about on the particulars, but can get much harder to fit in your head. So there's already a penalty for trying to gain easier reasoning properties through abstraction. So I don't think there's anything inherently easier to reason bout in type systems or declarative specifications or whatever. Types are only useful because they are simpler and smaller, and thus easier to reason about, than your code, so you can use them to double-check your code. They're like a checksum that way. But you can still get lost in types, or get them wrong, or put a bug in your type system, or struggle to reason about the type level invariants.

So in fact the more complex you make your types – especially the more specific behavior and invariants you encode into them, as in dependent types – the more the properties of types that make them a useful sanity check will evaporate, until types are no better (or different) from the code that you were trying to check, because they're encoding just as much behavior, and are just as complex and sprawling to keep track of, and you've just pushed your problem another step back, because the type-level language itself will need a type checker. As Simon Pyton-Jones, creator of Haskell, says:

There are programs you can write which can't be typed by a particular type system but which nevertheless don't "go wrong" at runtime, which is the gold standard - don't segfault, don't add integers to characters. They're just fine.

I think to try to specify all that a program should do, you get specifications that are themselves so complicated that you're not longer confident that they say what you intended.

And this isn't something you can really avoid in dependently typed languages: in them, your sanity-checking system (your type system) is your entire, full, term-level programming language, except the entire thing is lifted up one level of abstraction because now it operates on types as values instead of concrete values! This means that the upper bound of the easily accessible complexity of your type system is now the same as your code. And if you're the first type of programmer, then you're going to want to prove all the behavior of your code correct, which means a nearly 1:1 correspondence between your code and your types, which means you're going to always be asymptotically approaching dependently typed languages, and using those types to their maximal amount.

The second problem with formal methods and dependent types is that they don't take into account the real world nature of programming in most cases.

First, most programming is not done in a domain where the requirements and design goals are well understood enough in advance that a specification can be written up front. The actual human beings who are asking for the software to be built won't be able to just sit down and create a perfect idea of what they want the end product to be in their heads. They're going to want to give an initial direction, and then iterate in conjunction with prototypes produced by the software development team. Formal methods are deeply hostile to this. They want all of the basic properties and features of the system provided up-front, so that you can either derive a verified program, or verify and existing program, using them; moreover, they'll want a complete and internally-consistent design from the start, when we're not even going to have that to begin with.

And any attempt to try to get the customers to plan out everything in advance – as some particularly dogmatic FM people might be tempted to argue, with shades of Djikstra – is likely to lead to disaster: not only will they ask for the wrong things, things they don't want or need, the process will likely take so long that their actually requirements will have changed by the end – or the entire project could've become obsolete by that time. This is not even to mention the fact that if customers, or even programmers, are given free reign to design what they think is needed up front, they're likely not going to be able to accurately estimate what will be possible to implement, and so they'll end up with a giant stack of things you can't possibly actually do, instead of going out and prototyping each feature quickly and getting a sense for the problem.

Second, as programs develop, our knowledge of the specific domain, and how to solve problems within it, evolves. This means our program's ontology, including the data structures, functions, and software architecture it uses to model the domain, will need to change drastically many times over the course of development before they reach their final form. Programming isn't just rote, mindless construction work. It's often an exercise in design and applied ontology, and problem domains are often nuanced and complex enough that that work can't be done going in – there are too many unknown unknowns. Programmers need to be free to experiment and explore and prototype during the development of a piece of software. Any static type system will significantly hinder this kind of code, but more rigid ones, or anything that requires code to be perfectly correct by construction, will be worse for this.

Third, requirements change over time, even after the first release of a piece of software. If the way your software is written requires it to be this perfect, beautiful piece of logic, then it is going to be incredibly brittle and non-extensible if any changes need to be introduced that fall outside of the narrow set of requirements that have already been predicted. Any choice in how you model things with types and formal methods essentially makes strong assumptions about what the future requirements of the software can be allowed to be, locking off whole swaths of the future.

Of course, the point I'm not trying to make here is that, as a result, we shouldn't use formal methods, or even depedendent types, at all. What I'm suggesting is merely that formal methods and powerful type systems such as dependent types have significant tradeoffs, and that as a result they shouldn't be viewed as "just good software development practice" or "the inevitable future" or as an "inherent good," and should not be applied like religion where more abstraction and complexity in your types is viewed as an inherently good thing. Instead they should be used carefully, on a case-by-case basis, when merited by the software's domain, and most people should consider 80/20 alternatives such as randomized property-based testing, gradual typing and schemas, deterministic simulation testing, design by contract, simple ML-like type systems used responsibly, and lightweight model checking when necessary with things like TLA+ or Alloy.

Notice that a lot of my suggestions here work by verifying that some code you've actually written is correct after the fact through checking, instead of proving it correct by construction as formal methods and type systems do. This is because one of the most important things about problems in fields such as mathematics, computer science, and programming, is that merely checking that a solution is correct is a lot easier to do, both computationally and mentally, than constructing a provably correct solution.

Moreover, checking doesn't require any kind of meddling with the interior implementation or even architecture of a software component – it can treat components, subsystems, or even whole systems as complete black boxes, which you are free to add extra features to, rearchitect, or optimize at will, while continuing to verify whatever properties you thought were important enough to test, preserving the flexibility necessary for most software projects. While this approach is of course less powerful, with randomized property based testing, deterministic simulation testing, and design by contract you can be thorough enough to get 80% of the benefit of proof by construction, and crucially, with a much lower cognitive and labor burden. This is essentially the crucial distinction between the kinds of methods I endorse, which either only require very basic and easy proof by construction (such as an ML-family type system) or focus on checking things, when compared to dependent types and most formal methods, which operate by full proof by construction.