> AFAICT, our only hope is to build large software out of small components that can only be composed in obviously correct ways, so that the bulk of the verification effort is spent on each individual component, rather than on their interactions (a hopeless task).

But Schnoebelen's theorem proves this is impossible. (in my post: http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...)

The post also has an example of that: the foo/bar program, AKA Goldbach's program. bar is correct (i.e., it correctly decides whether its parameter is a prime -- maybe there's a bug in my implementation, but we can assume it's correct). This leaves foo. The first two lines are trivial. This leaves the next three lines (I guess that in Haskell it would be one line). I don't see how you can get more modular and composable than that! And yet, we haven't been able to prove the behavior of those three lines for 300 years, even though they're nothing but a simple decrementing for-loop, a single subtraction operation and a single disjunction! Why? Because bar (i.e. `prime?`), in spite of being correct, has a very complex behavior; it can be reasoned in some contexts, but not in this one.

In any event, every attempted project decomposed the problem as much as possible. The task still proved prohibitively expensive (although maybe not for high-assurance development!).

> The other view pays attention to how computation can be structured and given useful meanings

Almost, but not exactly. The values in machines matter greatly to the machine. The language models are human centric, i.e., they compute with values that matter to humans. But the important point of the post is that the two views are incomparable, as the second requires significantly higher work, i.e., expressing a computation in a way that's meaningful to humans is in itself a significant computational effort.

>and that it's useless for reasoning about time (for which there is no solution).

And that it doesn't work on real world systems. You can reason equationally about the gravity equation all you like, and compose as many instances as you like. But that wouldn't help you to decide interesting properties.

> On the other hand, the verification style you advocate, by looking directly at state transitions

I don't have an aesthetic reason to advocate this style. I'm a pragmatist, so I chose it and advocate it because it is the only style that has so far proven to work. That you can pick it up in a week or two instead of six months, and that it supports automated tools that make verification affordable are also great pragmatic advantages. If you show me another one that works as well on real-world systems, I'll be happy to use it.

> and that it doesn't gracefully handle computations whose state is split across several modules, none of which should inspect the state of the others

I'm not sure how you get that. TLA+ handles composition very nicely. There are operators that specifically hide variables, called temporal existential quantification. The formula basically says, "there exists a behavior over these (hidden) state variables, such that those other (observable) variables satisfy X".

> Do we have an equivalent of Lagrangian or Hamiltonian mechanics, to be able to relate both styles?

That's above my pay-grade, but TLA can be embedded in FP (in fact, the standard Isabelle distribution contains an embedding of TLA+, as TLA+ uses Isabelle as a backend prover, and I think there are embedings in Coq, too[1]), and FP can be embedded in TLA by conisdering extensional equality only. It's mostly a matter of convenience, possibly for different classes of problems.

The thing is that deductive proofs of any kind so far seem untenable in all but extreme circumstances. The problem with approaches that rely on types (and this may be orthogonal to FP, maybe not) to prove interesting logical properties are more rigid, and less able to accommodate more partial forms of verification. Maybe there's work on that, though. As a result of that, the TLA approach (in a general sense) is simply more battle tested, and with better real-world results.

[1]: http://ucsd-pl.github.io/veridrone/papers/memocode2015.pdf