For me, notation is everything. A computer program is a model of a problem. There is more than one representation of that problem: in the static code and in the running code. If you go to a kind of naive way of writing programs (that we all went through when we were first starting out), you write the code and then you step through it (either on paper, or with a debugger), viewing how the code is running.

There are many techniques available for helping you reason about your code. However, it's important to understand that software code is a notation for modelling the problem. Often formal methods introduce another notation that proves that the encoding of the problem in the first notation is "correct" according to some definition of "correct". The more we move into modelling the correctness in the second notation, the more we move the burden of reasoning about the issue to the "code" in the second notation.

It's often very useful to model the problem more than once. For example, I'm quite a big fan of unit tests. "Give the code in the system, I expect X to be true/false in this situation". I'm just as likely to make mistakes in my unit tests as I am with the production code. However, it's the comparison of the two that allows you to reason effectively about the code. They are two sides of the same coin (intentionally coupled -- which, as an aside, is why you should avoid trying to decouple your tests from your production code!!!).

Even though it is useful to model twice, I'm not really sold on the idea of doing it in general (and I have a very specific idea of how to write unit tests that's heavily coloured by this point of view). Everything that you add to the code should make reasoning about something easier and more convenient than not doing it. Otherwise you are better off with just writing the production code. You will have less complexity to deal with overall.

In my opinion, a good example of a tool that helps incredibly well are strongly typed languages with type inference systems. For a small penalty of type notation, the system can tell me, without a doubt, when I've made a mistake with the types of my variables. Not only that, but the notation itself allows me to reason about why I've gotten myself into a problem. It can even help me reason about what the function does, without having to even look at the implementation. This is incredibly helpful.

I think as we go forward, we need to be looking for this kind of tool. Dependent types seem like a perfect example of this. However, there is always going to be a small price to pay. Writing code in a statically typed language is harder than writing code in a dynamically typed language -- precisely because the dynamically typed language allows you to write code without having to think up front about the consequences. Of course, you may leave bugs in your code because of it, but the initial cognitive load is smaller. Similarly, it's much better to write code where you can reason about the run time behaviour without it running, but that is much harder than writing some code and walking through it, playing "computer".

We need to balance these kinds of factors because a tool that is not used is a useless tool. I'd be perfectly happy to work in a pure functional, statically typed language because it is much easier to reason about my code. Many of my colleagues simply are not willing (or possibly even able) to pay the upfront cost of working in that kind of ecosystem. Hence, I'm not able to work in it either.