On Two Views of Computation in Computer Science

> That's a good question and I don't think anyone has a definitive to that. I certainly don't. I think we should do empirical research and try to find out. What would be your guess and why?

I have absolutely no idea. The entire focus of my software development philosophy for a decade or has been to make programs easier for humans to understand, not easier to write proofs about (although there's some overlap). I do wonder how big the weak but extremely useful class of properties (like Rust's memory safety) is.

> After you verify a TLA+ specification, you still have the rather large task of making sure your actual program satisfies the specification. In this case, why should I bother verifying something that isn't the final program?

Theoretically, you can verify the program itself in TLA+, in a manner similar to how seL4 verified their code. You compile your final code to TLA+ to produce a low-level spec that captures the actual semantics of your progam, and check that it is a refinement of your high-level spec. Research teams have done this for Java and C (http://tla2014.loria.fr/slides/methni.pdf). The problem is that it doesn't scale, and neither does any other form of end-to-end proof. Humanity has never been able to formally prove an actual program that is anywhere near what we would call "large".

The reason you'd bother doing it is that 1. unlike end-to-end verification it is not only affordable, but also reduces costs, and 2. it actually works in uncovering the most costly problems, as verified by years of experience in industry on large projects.

> The program can be generated from the specification.

Ah, that is an interesting research question. Obviously in some cases a program could be generated. The spec would need to be deterministic for one (or nondeterministic in a way that makes sense for an actual program, like when representing multiple processes), computable (you can easily specify a program that takes an arbitrary program as input and says, "in the first step, let x be equal to TRUE if the input program terminates on the input 13, and FALSE otherwise"), and pretty low level because you can easily write things that would be extremely inefficient to run (like "let x be the smallest prime that's the sum of three squares" or something). Lamport believes that it may be possible (for a properly amenable spec) using machine learning. But it's not like compiling any high-level programming language.

> It would be a lot more cost-effective if we used languages, libraries and even operating systems geared towards formal verification.

Research doesn't seem to indicate that it would be, or rather, even if it is a lot more cost effective, it is still beyond affordable for all but high-assurance software, and high-assurance software already makes use of such languages (SCADE and SPARK work very well). But even in high-assurance, the industry doesn't bother with deductive proofs, as model checkers are automatic and work where they're most needed (SCADE) and SMT solvers are also reported to be effective for very restrictive languages (SPARK, but I've never tried it). Manual deductive proofs are used sparingly, to tie together results from automatic verification processes: http://events.inf.ed.ac.uk/Milner2012/J_Harrison-html5-mp4.h...

> 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

He mostly talks about proof assistants for general mathematical theorems, something I don't use, but in TLA+, proofs are of logical formulas, the steps are logical formulas (unlike in dependently typed provers), and a computation is just a (temporal) logical formula, so TLA+ already lets you incorporate computations into proofs, but the process isn't automatic. Then again, TLA+ isn't really designed nor used as a general theorem prover (though it certainly can prove general mathematical theorems) but as a tool to specify and verify algorithms.

Because Coq was designed (as I understand it) to help people prove theorems about mathematics, not about algorithms. If TLA+ -- a language designed to prove theorems about algorithms, not about mathematics -- is actually better for that purpose then a lot of people have wasted a lot of time.

Sure, algorithms are mathematical and much of mathematics can be recast as algorithmic, but still they have quite a different flavour. If a tool designed to help with one is actually the best tool to to help with the other, then that is astonishing.