> The goal of making imperative programs correct with formal verification with optionally other methods.
Yes, but correct at what confidence level, given that the higher the confidence the greater the effort, and 100% is generally impossible?
> SPARK handles it best right now
Again, I don't know what you mean by "best". SPARK is a limited language, and there are other limited languages that are even more amenable to verification than SPARK (e.g. SCADE). There's a whole bunch of tradeoffs, and it's unclear how you rank them, saying that one tool is "best".
> Partial verification with memory- and concurrency-safe language would be great.
Again, you're mixing several concepts here, and it's unclear how you rank them. You can ensure memory and concurrency safety with or without language support, and it's unclear what you mean by "partial verification". For example, you could say that guarantees for memory safety and no race conditions are a good sweet spot.
> The claim is incorrect for things such as SPARK which are designed for real-world use
Right, but JML tools are not behind SPARK, and it's unrealistic to expect people to use SPARK for general-purpose programs, as it is not quite a general-purpose language. Also, have you actually used SPARK on a large project yourself? In formal methods, the greatest advocates of certain tools are very often those who have never used them. When you do, you start seeing their limitations, and understand how no specific tool is a panacea and that no tool is "best" for all or even most purposes.
> It might be more or less work but it can be done.
For a very special kind of "can". seL4 is a 10KLOC C program that has been drastically dumbed down, and still took 20 man years! The people who worked on it told me that they believe it could now be done in 5 years, but even 5 years for an extra-simplified 10KLOC program is well beyond practicality for the vast majority of software.
> I'm pretty sure an amateur w/ some training can use a combo of spec-based checks and partial proofs to raise its assurance, though.
That depends on what you mean by amateur and by how much the assurance is raised. For example, SPARK simply cannot express global correctness conditions, let alone check them. Clearly, when you write a database and want to ensure serializability or no loss of data on failure, those are the most important properties by far. This simply cannot be done with any code-level tools -- like SPARK or JML -- certainly not feasibly.
I haven't tried SPARK myself, but I have tried JML with OpenJML, which is very similar, and I agree with Amazon that TLA+ gives you a bang-for-the-buck that is probably an order of magnitude greater than other approaches. Of course, you can then apply JML to code-level.
> I still want your references on global, composable correctness possibly being impossible to verify in large programs to be debated by top minds (including skeptics) in the field. Needs way more focus to help us determine how much future activity would be a waste of time/money.
There is no point to debate something that has been proven, but there's a big difference between what's proven in principle and what happens in practice, going both ways. It is certainly possible that even though correctness provably doesn't compose, it still turns out that for most programs people write, there is an affordable way to verify them. As there is no research -- as far as I know -- that tries to classify what constitutes a "reasonable program", the only way to know is simply to try various methods. To date, we simply have not been able to verify a large program end-to-end, and have not been able to verify small programs affordably. This is a simple fact. It is certainly possible that research will eventually find an approach that works, but it's not like we have a solution for real software today.