[ebiederm]

Have you looked at ADA Spark?

If you have does it match your intuition of how things should be done?

I am slowly working on something where I hope to integrate such a capability for the things that type systems can't handle quickly.

So I would be interested in perspectives of people who have been down this route before.

[Animats]

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.

[rramadass]

Have you looked at "Verified Design-By-Contract"? See the paper Safe Object-Oriented Software: The Verified Design-By-Contract Paradigm by David Crocker here - https://www.eschertech.com/products/verified_dbc.php

David Crocker's Verification Blog - https://critical.eschertech.com/

[ebiederm]

Not who you asked but I took a quick look.

Typically Design by Contract has meant runtime assertions. I like that they are doing verification before runtime.

At the same time their take on loops (you can't write them and have verification puts me off). Especially when modern c++ has so many prebuilt looks. It would seem to me it should just be a matter of annotating the prebuilt loops and encouraging their use.

I think their approach will fail on modern encryption code because it takes too much control (loops) from the programmer.

[rramadass]

Which paper did you read? The "Safe Object-Oriented ..." one that i pointed to or something else? Crocker's writings explain a lot more especially w.r.t. usage with C/C++.

See for example Can C++ be made as safe as SPARK? - https://www.eschertech.com/papers/index.php which identifies a subset and enhances it with annotations. This can be updated with his later article Contracts arrive in C++26! - https://critical.eschertech.com/2025/09/09/contracts-have-ar...

Also see articles under Proving C and C++ programs correct - https://www.eschertech.com/articles/index.php

Animats was bemoaning that OO has declined and that you needed object/DS invariants. I was pointing to the fact DbC has it all (people should always use the runtime checking approach) and with Verified-DbC you could do it statically too. Formal Methods can be done at various levels and a developer can choose and adopt what he feels comfortable with initially before graduating to fullblown heavyweight methodologies/tools. What is needed is developing Formal Method Thinking. See the paper On Formal Methods Thinking in Computer Science Education linked to here - https://news.ycombinator.com/item?id=46298961

[int_19h]

Rust proc macros are good enough to have design-by-contract implemented in them, although for type invariants it's not exactly ergonomic (because you have to disallow inner mutability to avoid someone grabbing a reference to a field and then mutating it without any invariant checks).

I don't know if there are any solutions combining this with static analysis. Of course, even the runtime checks are very helpful (doubly so in AI-written code).

[ebiederm]

Thank you. That makes things clearer.

I especially appreciate the trick of asserting the intermediate truth to help the prover along.

As someone who writes software I very much agree that verification of asserts before run time (written in the language itself) is very approachable to a programmer.

In a similar vein I agree with the folks at Jane Street that aiming to rule out specific classes of bugs (as opposed to proving a program is entirely correct) is a very practical goal.