The trouble with formal specification, from someone who used to do it, is that only for some problems is the specification simpler than the code.
Some problems are straightforward to specify. A file system is a good example. The details of blocks and allocation and optimization of I/O are hidden from the API. The formal spec for a file system can be written in terms of huge arrays of bytes. The file system is an implementation to store arrays on external devices. We can say concisely what "correct operation" means for a file system.
This gets harder as the external interface exposes more functionality. Now you have to somehow write down what all that does. If the interface is too big, a formal spec will not help.
Now, sometimes you just want a negative specification - X must never happen. That's somewhat easier. You start with subscript checking and arithmetic overflow, and go up from there.
That said, most of the approaches people are doing seem too hard for the wrong reasons. The proofs are separate from the code. The notations are often different. There's not enough automation. And, worst of all, the people who do this stuff are way into formalism.
If you do this right, you can get over 90% of proofs with a SAT solver, and the theorems you have to write for the hard cases are often reusable.
Programming is very similar to inductive reasoning, you establish some facts, do a step that changes something, and establish facts after the step and then repeat that with different steps until you get the facts you are after. (See e.g. Manber's book.) If you merely set out to rigorously write the computation steps, the result will already be a proof sufficient for a human. I am not sure, but I think Dijkstra ended up doing or maybe just writing about something like that, he wanted to get programs that were correct by construction, not proven to be correct afterwards.
What is utterly lacking is a formal notation for these computation-reasoning steps that is not tied to a specific programming language. As a result what we get now is an informal specifications and a bunch of different final implementations for different languages. Whatever knowledge could be kept is not kept in any organized way.
No, formal specification helps from the get-go. You can iterate more reliably, thus faster. The successful development of mathematical theories depends on having rigorous definitions and proofs all the way from the start so that people can communicate effectively, point out caveats unambiguously, and modify the theory robustly. Without formal specs/proofs, refactoring will become too hard. It's actually a lot easier to capture the behavior of a program formally than by tests. Programmers need to gain some experience in math to see this. Listen to Hoare and Dijkstra, and start "thinking".
I predict in 10 years „code“ that is not actually in the language of a proof assistant will be the exception, not the norm. This will happen by proof assistant languages becoming easier to the point that normal code will look cumbersome
I'm always skeptical of claims like these. Ultimately, programming is about writing down instructions for computers to follow. Existing programming languages evolved to be ergonomic for that, proof assistants less so.
And having meta language that is significantly different from the core language really sucks for ergonomics. I never understood why, for example, a lot of dependent types literature invents a meta language for expressing constraints rather than using the core language for it. Syntactic familiarity matters.
Also consider C++ templates vs Zig comptime, and how C++ is evolving to bring its meta language closer to the core language via constexpr and consteval.
So the more viable path is to judiciously integrate formal concepts into "normal" programming languages and have LLMs generate proof artefacts in a search process that is guided by proof systems.
> There exists a higher level problem of holistic system behavior verification
This is the key observation. Strict, code-level verification of every line, while valuable in the small, doesn't contribute very meaningfully to understanding or building confidence in higher level system properties.
I see a future of modules with well defined interfaces and associated contracts. Module level contracts can be formally verified or confidently believed via property based testing. Higher level system behavior can then be proven or tested by assuming the module contracts are upheld.
Module boundaries allow for varying the desired level of confidence module by module (testing, property based testing with variable run time allotments, formal verification).
LLMs can handle each step of that chain today, allowing humans to invest specifically where we want more confidence.
Formal verification methodologies are more important than some cure-all, one-ring-to-own-them-all specification.
Formal specification by itself has been tried and failed as far back as Z notation. This is a perennial problem that cannot be solved with a panacea single specification standard because it is a process problem requiring a suite of tools to verify the products plus human habits, intention, and human effort to achieve, maintain, and improve upon excellence. While standards, simplicity, and uniformity help, there is still much too much irreducible complexity and minutiae that cannot be wished away by some sort glorified Cucumber testing or inventing the N+1 thing on top of (Isabelle, Idris, Coq, etc.) that wasn't invented here.
An uncomfortable truth is that 99.99% of current software development is nowhere close to rigorous. This isn't remotely a good thing™, especially for essential components.
13 comments
[ 3.5 ms ] story [ 32.4 ms ] threadTest tables and scenarios may not cover all the things that can go wrong (a la Goëdel), but not doing them almost guarantees broken software.
Some problems are straightforward to specify. A file system is a good example. The details of blocks and allocation and optimization of I/O are hidden from the API. The formal spec for a file system can be written in terms of huge arrays of bytes. The file system is an implementation to store arrays on external devices. We can say concisely what "correct operation" means for a file system.
This gets harder as the external interface exposes more functionality. Now you have to somehow write down what all that does. If the interface is too big, a formal spec will not help.
Now, sometimes you just want a negative specification - X must never happen. That's somewhat easier. You start with subscript checking and arithmetic overflow, and go up from there.
That said, most of the approaches people are doing seem too hard for the wrong reasons. The proofs are separate from the code. The notations are often different. There's not enough automation. And, worst of all, the people who do this stuff are way into formalism.
If you do this right, you can get over 90% of proofs with a SAT solver, and the theorems you have to write for the hard cases are often reusable.
What is utterly lacking is a formal notation for these computation-reasoning steps that is not tied to a specific programming language. As a result what we get now is an informal specifications and a bunch of different final implementations for different languages. Whatever knowledge could be kept is not kept in any organized way.
No body wants to pay that price when they are struggling with product market fit.
What actually happened was that some programming languages borrowed a few concepts and life carried on as before.
And having meta language that is significantly different from the core language really sucks for ergonomics. I never understood why, for example, a lot of dependent types literature invents a meta language for expressing constraints rather than using the core language for it. Syntactic familiarity matters.
Also consider C++ templates vs Zig comptime, and how C++ is evolving to bring its meta language closer to the core language via constexpr and consteval.
So the more viable path is to judiciously integrate formal concepts into "normal" programming languages and have LLMs generate proof artefacts in a search process that is guided by proof systems.
> There exists a higher level problem of holistic system behavior verification
This is the key observation. Strict, code-level verification of every line, while valuable in the small, doesn't contribute very meaningfully to understanding or building confidence in higher level system properties.
I see a future of modules with well defined interfaces and associated contracts. Module level contracts can be formally verified or confidently believed via property based testing. Higher level system behavior can then be proven or tested by assuming the module contracts are upheld.
Module boundaries allow for varying the desired level of confidence module by module (testing, property based testing with variable run time allotments, formal verification).
LLMs can handle each step of that chain today, allowing humans to invest specifically where we want more confidence.
Formal specification by itself has been tried and failed as far back as Z notation. This is a perennial problem that cannot be solved with a panacea single specification standard because it is a process problem requiring a suite of tools to verify the products plus human habits, intention, and human effort to achieve, maintain, and improve upon excellence. While standards, simplicity, and uniformity help, there is still much too much irreducible complexity and minutiae that cannot be wished away by some sort glorified Cucumber testing or inventing the N+1 thing on top of (Isabelle, Idris, Coq, etc.) that wasn't invented here.
An uncomfortable truth is that 99.99% of current software development is nowhere close to rigorous. This isn't remotely a good thing™, especially for essential components.
See also: seL4.