Formal methods and the future of programming

> Industrial logics are really practical and allow you to write all sorts of sophisticated properties that your system should satisfy in a very succinct way.

It sounds like what you think as positives are exactly the things parent comment thinks as negatives.

"Logic is to computer science and software engineering what calculus is to ... mechanical or civil engineering"

Things professionals rarely use in practice?

Thanks for the pointers to the papers.

One book which seems not that well known is Arindama Singh's Logics for Computer Science 2nd edition - https://www.phindia.com/Books/BookDetail/9789387472433/LOGIC...

For more details see author's webpage - https://home.iitm.ac.in/asingh/books.html

> TLA+, which has gained quite a lot of popularity

Why do you think that? Outside of just toy examples, and vague examples of "AWS uses that", I don't know of any actual code which has TLA. Most of the things you can do with TLA, you can do with informal math notation quite easily.

Do you have any real world long term usage examples?

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.

You're right. I think the point we need to discuss here is, to be clear, dividing the contexts in which defensive programming is strong and where it should be aggressive.

I think the overhead of implementation is enormous, but I believe AI can write it. However, before even reaching the 'implementation' stage, that is, at the planning stage, sufficient data must be collected for the implementation to be safe.

In that respect, I think Jane Street already has enough data and modeling capabilities. However, I think it's a bit difficult to say whether this approach will take shape in many other domains.

In that sense, I also think that the reason many industries are doing this kind of fast deployment and experimental tooling might be a preparatory step for that kind of modeling. Have a good day Thanks for the good comment. It helped me think more sharply as well

>Fwiw - you already use defensive everywhere. Python, Java, etc. come with garbage collectors. It's verified that the code is executing your intent.

Sort of. Garbage collectors can be fallible too, especially where release optimization is used.

However, I don't know things as deeply as you do; I only know the basic framework. So you're right that I don't know it deeply. If you have time later, please teach me that part, and I will gladly study it As you said, starting from the light parts and applying them directly might work better for me too. I would appreciate it if you could recommend a few books

I'm sorry, but what you've said are things I've already read.(this:https://research.tue.nl/en/publications/on-formal-methods-th...)

The points you're raising are not what I'm arguing.

What I am arguing is this:

Formal verification only guarantees consistency between the 'specification' and the 'implementation.' It does not guarantee that the 'specification' correctly reflects reality. This is a problem of modeling.

For your logic to hold, it would imply that humans can formalize, to some degree, the amount of loss that occurs when modeling reality. That is not possible.

It only tells you whether the implementation satisfies the specification. That's also what the OP's post is about. The point that 'the cost has been lowered due to AI' is largely no different from simply saying 'the cost of implementation has gone down.' The real question is whether that implementation properly reflects reality.

The OP's post is fundamentally about 'internal invariants.'

But if you look at the beginning of the first post: 'But outside of some special cases (notably, hardware synthesis), our sense has been that formal methods were just not worth the costs for us. And those costs are really high! seL4 is a great example of this. It's a formally verified microkernel, and a profound achievement. But, boy was it expensive to do! It took 25 person-years of effort to verify 8,700 lines of C, and each line of code required something like 23 lines of proof and a half a person-day to verify.' And the post suggests extending existing methodologies. I think a limited case and generalizing it are different problems. The point is that not every special case is general.

That is why I pointed out whether this extension of methodology is even possible. I am skeptical on this point.

If you want to criticize me, rather than talking about such methodologies, you should criticize the essence of my logic: whether even offensive programming properly understands modeling. I am not simply opposing the OP's post; rather, I am asking whether modeling in the age of AI agents is comparable to modeling in the past.

The materials you shared for me are helpful, but I am saying they do not align with my logic.

Your introduction says: '===== The Problem: Realism vs. Idealism =====' Right?

The question is whether the idealism you advocate actually reflects reality. I am simply arguing for modeling. The gap in my argument is that 'then, because modeling also changes frequently, couldn't all methodologies become useless?' That could be a potential flawed skepticism. But what you're saying is not that.

Every argument has a blind spot. But you are not reading the weak points of my argument; you are only reading your own strong points. This only creates friction and leads us to argue about our emotional differences. I think you are intelligent and knowledgeable. But the points you're raising are not the points of criticism I intended, and what you're pointing out is not what I said.

I am not saying that all methodologies are wrong. I am saying that a methodology can go wrong if it steps outside its boundaries.

However, the fact that you linked me to things I could study was, I think, a gesture of goodwill, assuming that I, as a junior programmer, was misunderstanding something and trying to help me learn. But criticism that assumes I just don't understand isn't helpful for either of us.

guy's korean, looks like? korean <-> english is the hardest language pair of two industrialized-nation languages, almost.

That's up to the harness. Right now, my harness doesn't have any tools that would allow the agent to change contracts. Also, agents working on a Rocq proof don't have write access to the C+ACSL code; they can review it, and propose structural changes to the coordinator, but all they can do is iterate on the Roqc proof or give up. The weakest part of the harness today is that the agents that do C+ACSL work can modify both C and ACSL, even though they're usually run with the explicit intent to not change the semantics of the C code (although it's totally within bounds, and often required, for them to change e.g. `foo & 3` to `foo % 4`) -- so there's weakness here, but it's bounded, and since the contracts live in header files that they can never write, it's worked so far. It's a starting point, at least; I certainly wouldn't say this is a mature, or even good, tool chain, but still learning.

With the proof checker.

Proof checkers fuel the AI hype by outputting "valid" for a hallucinated text. /s

The problem with that mindset is that testing, like verification, becomes extremely powerful as it becomes more automated and you throw more compute at it. And it's arguably easier to automate testing than it is to automate formal verification.

Sure, testing isn't perfect. But is finding 100% of the bugs that much better than finding (say) 99% of them? This is especially the case if the missed bugs tend to be those that happen very rarely.

A formal specification allows automatic generation of tests. So run billions of tests, randomly generated, and see if any violate the specification.

Even theorem proving systems use this sort of thing as a short cut, for example pruning off attempts to prove a universally quantified statement by looking for counterexamples.

>Of course, you have to define what "has the same behavior as" means

And that's really my issue, for example when you define "has no trailing whitespace", you are basically writing a piece of the implementation. Cover all behaviors, and you have basically re-implemented the function, no?

In other words, if I have the full formal spec of f(), isn't that the same thing as having f()?

  func hypot(x, y):
    return sqrt(x*x + y*y)

> But with formal methods, you can prove that "for any input x, foo(x) returns a string with no trailing whitespace".

Isn't that essentially property testing?

    x = x * x

    if x > 50:
      x = 42

    something_afterwards(x)

If you have an int32 or less you can!

This is all pre-release but a few highlights:

- `continuity` is a `lean4` metaprogramming system that we use all kinds of ways but the real meat is it allows formal specification of codecs and state machines in ways that make security and performance properties proof amenable, the key trick here is to limit parser power to just what you need and no more. a very cool thing is that we can add targets to it, so when we do Zig for example, Zig will immediately get proven correct and frontier performance support for dozens of protocols that are not all mature right now.

- `libevring-cpp` (bound up into `libevring-hs` and `libevring-rs`) is a Trinity-inspired deterministic event replay system that replaces anything you would have done with `libuv` or whatever, and it's wired into `io_uring` (we're stuck with `kqueue` on darwin, eh). it interfaces with `continuity` machines and codecs (which are generated very carefully for the hardware they run on) and we have yet to find a way of measuring such programs where it doesn't resoundingly shatter the performance of any other asynchronous programming primitive in any language. i'm sure the community will prove us wrong when we release it, but it's real fast. and you get much stronger guarantees than in most such systems (Trinity derived, so if you can repro a bug, you can walk the event trace until it's sitting there in GDB and shit)

- `hyperconsole-cpp` (and `hyperconsole-hs` and `hyperconsole-rs`) is the TUI library idea taken to some deranged extreme on performance and supports everything in `notcurses`, it's pretty wild: https://youtu.be/YqgEtpJ8tGI

- straylight-nix is a complete rewrite of nix that fixes thousands of bugs, hundreds of them security adjacent and dozens of them we only talk to vendors about. it's daemonless, dramatically faster, ground-up WASM-targeting compiler with a formal grammer, uses an extremely fast LSM-based store (it can read the legacy store but we don't write it) that fixes all the problems in floating CA, IFD is too cheap to care about, and recursive nix is no longer and issue (see daemonless). it supports tearing derivations into `REAPI` actions that you can feed to your friendly native NativeLink or whatever, which just goes through them like a woodchipper. KVM-based sandbox with snapshot and restore, really opens the world up on what your builders can be.

- `slide` is the reference implementation of a family of protocols called `SIGIL`: `SIGIL-LLM` is a binary encoding for LLM data that resets on ambiguity and drops the average bytes on the wire from e.g. OpenRouter to your harness from ~hundreds to ~1.5 per token, `SIGIL-API` is a bijection on OpenAPI 3.1.0 and AsyncAPI 3.0.0 that gives comparable improvements, and `SIGIL-SH` is such an encoding for a sensible subset of bash. this does about 1.5 billion tokens per second on a laptop and never emits partial frames, so you don't get speculative execution rollback problems in your harness that tilt agents off.

- `// WEAPON //` is an adversarial, vendor-skeptical, full-take surveilance agemt harness built on `hyperconsole-cpp` and `SIGIL` (so, you could absorb the entire token output of OpenRouter on one machine if you wanted at least on the wire and in the terminal, clearly the bottleneck rapidly becomes whatever the agents are calling, but it's `zmq4` transport underneath `SIGIL` so it's also trivial to full-take all of your data for fine tuning or whatever you want it for into e.g. `parquet` on R2. `// WEAPON //` does a bunch of stuff: the tool call surface is heavily optimized for AST-level edits that miss dramatically less, we intercept and manipulate shell commands (slice off the stupid `| tail -n5` that keeps the droid in a loop not seeing the error, pre-emptively ground using heuristics that have been tuned (defeats the search flinch), and always recovers from any stall, or nag box, or anything else that would serve as an unannounced rate limit, it's fine if vendors rate limit but they need to put it in their ToS. it has a bunch of other primitives, agents run in real KVM sandboxes and speculate out as wide as you want to pay the tokens for. we hyper-manage things like the cache breakpoint geometry of Anthropic so e.g. Opus rarely misses in cache and always hands off edits to specialized tool use models. it's pretty extreme the difference in outcomes relative to all this React jank.

- `s4` is a general-purpose compiler from most any pytorch 2.0 model to `myelin`-level performance on NVIDIA (we only support NVIDIA Blackwell at the moment, that might change) and it's never worse than `myelin` because if we don't out-tune it we invoke it, but we out tune it a lot because we've proven a lot of decideability theorems about tiling and scheduling on both 1CTA and 2CTA, so we can often arrive at a finite, enumerable set of schedule/tile choices. `myelin` mops up the random garbage around the big GEMMs just like in TRT-LLM.

- `sigil-trtllm` is inspired by TensorRT-LLM-Edge but designed from the ground up around Mellanox/ConnectX and in particular GPUDirect, so it can stream `SIGIL-LLM` tokens directly onto the wire whereas something like Dynamo is usually traversing both Python and NATS, which is super weird to us. this uses the `s4` compiler very heavily.

- `straylight-cas` is a geographically distributed content addressable store backed by any R2-compatible (so most any S3-compatible too) object store with multi-level LSM and extreme performance memtables, optimistic hinted handoff over `zmq4` to other geographies, and a really simple operational story, this is kind of the thing that powers the product surface.

... which is the thing i'm less ready to talk about because it's supposed to be a surprise.

So, formal methods produce runnable systems, but communication remains the challenge.

If a formal spec is messy, then it's a proof of ... what, exactly?

A formal specification that bridges tech and product, that lets non-technical contributors read and discuss all the logical nuances, directly as operational code, at product's level of abstraction of interest, would transform a lot.

It's no longer a challenge to create code, it's a challenge to create business requirements and translate them into systems.

The problem is that generating either code or proofs with LLMs is very expensive, and generating good proofs (I don't mean elegant, I mean proving the most important properties) is probably not very fast, either. Reducing the verification time of a program from 100 years to 10 years or the cost from $1bn to $100m is still not practical enough to become truly mainstream.

Things can be improved when people help guide and focus the LLMs, but these people still need to be formal methods experts.

> One can make the argument that the requirements is a much smaller surface to verify than that of the entire program.

This argument is unfortunately empirically false for any program of any meaningful complexity (>1000 lines, probably even as low as >100 lines ignoring well-defined algorithms and data structures) using current formal methods.

Complete formal specifications are usually multiple times larger than the corresponding source code and encode esoteric propertys necessary for the proof, but which are largely even more impenetrable than a undocumented codebase.

So, it is both harder to figure out if you encoded the desired requirements and it is more complex. Your only advantage is confidence that what you wrote down is proven.

But don't you still have to logically connect the validity of the proof to desirability of the output?