Formal methods and the future of programming

Formal verification is a mathematical proof and requires axioms. However, if real world field data is not collected, you are not comparing theory to reality but forcing reality to fit the theory, like the bed of Procrustes.

This means the object of verification is not reality but the consistency between specification and implementation, and incorrect formal verification only refines a wrong worldview.

A company with sufficient capital can turn a theory into reality through marketing and other means. But for small businesses or in markets where new competitive logic is introduced due to the lifespan of an industry, this can be a fatal problem.

For example, consider the stock market. If you use the Buffett indicator to invest right now, the market looks overheated. But other indicators suggest positive prospects. We cannot know whether the market logic of the AI era aligns with the past or is different, but I believe there are cases where modeling changes due to real world shifts.

In reality, when converting the real world into mathematics or physics, information loss is inevitable. In this process, science may later advance and become more precise, or a value once considered important may turn out to be wrong.

In other words, something may be correct within a given set of axioms, but those axioms themselves may change depending on the context. The history of computer standards has shown this as well(ASCII -> Unicode)[To explain this point, ASCII works perfectly in English speaking countries, but in my country it creates incorrect encoding.]

Programmer's ability may come down to distinguishing between what changes little and lasts long, and what changes quickly

After writing the replt, I realized I was being too critical of formal verification. I think Jane Street's argument holds for invariants inside code. However, I am cautious about whether that logic can be extended to other fields. I haven't studied deeply enough, so my thinking may be shallow. Please understand

I am super interesting in `straylight-nix`. Even a blog post on what you did to improve it would be elucidating.

I've generally liked classic approaches which had entry and exit conditions, and loop invariants, all written using the same syntax and operators as the program. The compiler has to know what to ignore, of course. The compiler should syntax and type check all the proof information, even if it can't verify it. It's important to avoid an impedance mismatch between the proof system and the programming language. If programmers are constantly translating between two notations, customer resistance will be high.

If you need to write functions as scaffolding for proofs, they should be written in the programming language. You might need some operators that aren't actually runnable, such as FORALL, but the syntax should be that of the programming language. If your specs look like

    Γ, P || Q, P ==> R, Q ==> R ⊢ R

in a language with none of those operators, you're doing it wrong. That's the disease of falling in love with the formalism.

The user should not have to tell the proof system things the compiler already knows. Whatever overloading and aliasing rules the language enforces should be known and handled in verification, too. We worked off the syntax tree produced by a compiler front end modified to handle the verification statements, not the raw source code. Ada Spark has different aliasing rules than Ada, for example.

One big problem is that object oriented programming came and went in popularity. You really want object invariants. You need some way to attach an invariant to a data structure. You also need a clear boundary where control enters and exits the objects. If the language doesn't have objects, you struggle with trying to express object type invariants in the proof language. You don't get the boundaries as part of the programming language.

A useful interface between the prover and the program is simply to use

    assert(A);
    assert(B);

in the middle of code to encapsulate complex proof goals. A should be provable from the preceding code using a SAT solver. B, when assumed true, should provide enough info for a SAT solver to proceed from that point. Now you need to prove

    A implies B

by external means. That creates a well defined problem which can be given to something AI-like, backed by a proof checker, to chew on.

Ada Spark has some features that violate these rules. Also, it's hard to find anything about Ada Spark newer than ten years old.

There's a fair amount of interest in verifying Rust. There's been some progress using Dafny. But "Dafny is not Rust. Using Dafny requires porting algorithms of interest from Rust to Dafny. This port can miss details and introduce errors." There's the impedance mismatch again. Verus looks more promising. It is more Rust-like in syntax, they get the SAT solver/AI prover distinction, and there's active development.

I am not sure that the perspective you have taken is the same as what I understood from the parent post; what I took from it is that things like registers, memory locations, ways to implement square root, and so on, are all _implementation choices_ that are not important properties of the specification. You specify that the hypotenuse is the square root of the sum of squares, but whether square root is implemented using Newtonian approximation or a fast inverse square root is irrelevant; whether your first argument is passed in a register or on the stack is irrelevant.

Often, things like resource usage are not specified: running time, memory consumption, etc, aren't relevant enough to appear in a behavioural specification.

If your spec says "f(a, b) returns a + b", but it's just a high-level document you can use to help guide your implementation, integer overflow is just one of many ways your implementation might be inconsistent with the specification. It's still likely that the existence of a formal specification you reference during implementation means that more edge cases have been considered ahead of time than if you just had an informal spec.

If, on the other hand, you prove it but it turns out not to be true (ie, you overflow integers), your proof is wrong. If a machine verified your proof and gave you a big thumbs up, your machine verification is wrong.

If, in Idris, I write "f : (a : Nat) -> (b : Nat) -> (c : Nat * c = a + b)", then I cannot compile an implementation for which I can't show a proof that the result is _always_ the addition of a and b, for all a and b, unbounded by anything but the resources at hand with which to run the program. An implementation subject to integer overflow won't compile.

Or, I could write "f : (a : Bits32) -> (b : Bits32) -> (c : Bits32 * c = a + b)" and implement something where , but then modulo arithmetic on overflow is _part of the specification_, because "+" in there is doing the heavy lifting of being defined as addition modulo 2*32 already; by specification, 4 billion plus 4 billion is ~3.7 billion.

It's also possible it's not the future of programming.