6 ms·

The Coming Need for Formal Specification

64 points by todsacerdoti 11mo ago

readthenotes1 11mo ago
Some realized that building the tests was the more important part of writing the software long ago... Test 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.
- skydhash 11mo ago
  And designing your code for easy testing also almost always guarantees that the code will be maintainable.
jackblemming 11mo ago
Whenever you look closely at what these proof nerds have actually built you typically find… nothing. No offense to them, it’s simply reality.
- AlotOfReading 11mo ago
  SeL4, a number of mathematical theorems, a bunch of cryptography. You've likely trusted your life to compcert. It's not nothing, but it's admittedly a bit limited. Formal methods are the hardest thing in programming, second only to naming things and off by one errors.
- atomicnature 11mo ago
  Leslie Lamport built latex, most of distributed systems such as AWS services depend on formal verification. The job of Science here is to help Engineering with managing complexity and scale. The researchers are doing their jobs
  - ofrzeta 11mo ago
    What does LaTeX have to do with TLA+? Also I think "most of distributed systems such as AWS" might be an exaggeration. At least the public known examples of formal verification in AWS are scarce.
    - MangoToupe 11mo ago
      I think the implication is that Lamport is a proof nerd, not that LaTeX has a direct relationship to proof software.
    - justincormack 11mo ago
      AWS talk about it a fair amount, although rarely in a lot of detail.
- scrubs 11mo ago
  I see no need to dunk like that. There are ample stories over the years on HN how software orgs without using FM have bugs, waste money, treat people poorly, all leading to canceling software projects before delivering anything to customers. And I'm only mentioning just a very few issues. Software development in corps has many challenges to ROI and customer satisfaction. I might also point out FM had a nice history of value-add in HW. And we know HW is higher quality than software.
Animats 11mo ago
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.
- akoboldfrying 11mo ago
  > Now you have to somehow write down what all that does. I think the core difficulty is that there's no way to know whether your spec is complete. The only automatic feedback you can hope to get is that, if you add too many constraints, the prover can find a contradiction between them. But that's all (that I'm aware of, at least). Let's take an extremely simple example: Proving that a sort algorithm works correctly. You think, "Aha! The spec should require that every element of the resulting list is >= the previous element!", and you're right -- but you are not yet done, because a "sorting algorithm" that merely returns an empty list also satisfies this spec. Suppose you realise this, and think: "Aha! The output list must also be the same size as the input list!" And again, you're right, but you're still not done, because a "sorting algorithm" that simply returns inputSize copies of the number 42 also satisfies this new spec. Suppose you notice this too, and think: "Aha! Every element in the input should also appear the same number of times in the output!" You're right -- and now, finally, your spec is actually complete. But you have no way to know that, so you will likely continue to wonder if there is some additional constraint out there that you haven't thought of yet... And this is all for one of the tidiest, most well-specified problems you could hope to encounter.
rramadass 11mo ago
Nada Amin's research mentioned in another thread is relevant here - https://news.ycombinator.com/item?id=46252034 https://news.ycombinator.com/item?id=46252034
- seg_lol 11mo ago
  Nada Amin isn't relevant to hacker news, she is 15 years ahead of grifting tech bros.
  - rramadass 11mo ago
    Just to make sure that people don't get the wrong idea; Nada Amin's Harvard webpage states; I combine programming languages (PL) and artificial intelligence (AI), including large language models (LLMs), to create intelligent systems that are correct by construction. My current application domains include program and proof synthesis, and precision medicine. ... we look at combining Machine Learning and Programming Languages to enable the creation of neuro-symbolic systems that can move back and forth between learnable (neural) and interpretable (symbolic) representations of a system. She was a recipient of the Amazon Research Award 2024 for LLM-Augmented Semi-Automated Proofs for Interactive Verification - https://www.amazon.science/research-awards/program-updates/70-amazon-research-award-recipients-announced https://www.amazon.science/research-awards/program-updates/7...
Mikhail_Edoshin 11mo ago
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.
- mchaver 11mo ago
  I wasn't familiar with that book. For other users, I think the book they are referring to is Introduction to Algorithms A Creative Approach by Udi Manber.
- skydhash 11mo ago
  > What is utterly lacking is a formal notation for these computation-reasoning steps that is not tied to a specific programming language A formal notation for this is a programming language. Which is why everyone use pseudo code or something equivalent for a first pass thinking or for communication.
  - Mikhail_Edoshin 11mo ago
    Not quite. It is in a way (very visible when we talk about invariants), but it is not, well, semantic. A good notation for those steps would allow me to make only the distinctions I care for and ignore the distinctions I do not care for. So, for example, if I want to describe the greatest common divisor algorithm, I would only focus on the arithmetic part and define the domain of the parameters as "positive integers" (or maybe "non-negative integers"). A real programming language has a different goal: the code must run and do something useful. So I am unlikely to be able to define the domain like that (won't be able to make important distinctions) and, at the same time, will likely have to attend to things I do not care about (will have to make unimportant distinctions). All this will cripple and obscure the logic. This is what happens now and as a result we have a different implementation of everything for every programming language.
victor_xuan 11mo ago
Formal specification only works once the system are in a relatively final shape. No body wants to pay that price when they are struggling with product market fit.
- seg_lol 11mo ago
  formal > typed > untyped > unsound > vibed
- learningstud 11mo ago
  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".
auggierose 11mo ago
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
- pydry 11mo ago
  Back when I first studied this 20 years ago the progenitors predicted it would get very popular one day. What actually happened was that some programming languages borrowed a few concepts and life carried on as before.
  - auggierose 11mo ago
    I started with this 30 years ago, so yeah, I know the history :-) This time is different.
- atq2119 11mo ago
  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.
abrgr 11mo ago
Great article! > 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.
burnt-resistor 11mo ago
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. See also: seL4.
tug2024 11mo ago
[dead]

64 points by todsacerdoti 11mo ago

Some realized that building the tests was the more important part of writing the software long ago... Test 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.

skydhash 11mo ago
And designing your code for easy testing also almost always guarantees that the code will be maintainable.

jackblemming 11mo ago

Whenever you look closely at what these proof nerds have actually built you typically find… nothing. No offense to them, it’s simply reality.

AlotOfReading 11mo ago
SeL4, a number of mathematical theorems, a bunch of cryptography. You've likely trusted your life to compcert. It's not nothing, but it's admittedly a bit limited. Formal methods are the hardest thing in programming, second only to naming things and off by one errors.
atomicnature 11mo ago
Leslie Lamport built latex, most of distributed systems such as AWS services depend on formal verification. The job of Science here is to help Engineering with managing complexity and scale. The researchers are doing their jobs
- ofrzeta 11mo ago
  What does LaTeX have to do with TLA+? Also I think "most of distributed systems such as AWS" might be an exaggeration. At least the public known examples of formal verification in AWS are scarce.
  - MangoToupe 11mo ago
    I think the implication is that Lamport is a proof nerd, not that LaTeX has a direct relationship to proof software.
  - justincormack 11mo ago
    AWS talk about it a fair amount, although rarely in a lot of detail.
scrubs 11mo ago
I see no need to dunk like that. There are ample stories over the years on HN how software orgs without using FM have bugs, waste money, treat people poorly, all leading to canceling software projects before delivering anything to customers. And I'm only mentioning just a very few issues. Software development in corps has many challenges to ROI and customer satisfaction. I might also point out FM had a nice history of value-add in HW. And we know HW is higher quality than software.

Animats 11mo ago

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.

akoboldfrying 11mo ago
> Now you have to somehow write down what all that does. I think the core difficulty is that there's no way to know whether your spec is complete. The only automatic feedback you can hope to get is that, if you add too many constraints, the prover can find a contradiction between them. But that's all (that I'm aware of, at least). Let's take an extremely simple example: Proving that a sort algorithm works correctly. You think, "Aha! The spec should require that every element of the resulting list is >= the previous element!", and you're right -- but you are not yet done, because a "sorting algorithm" that merely returns an empty list also satisfies this spec. Suppose you realise this, and think: "Aha! The output list must also be the same size as the input list!" And again, you're right, but you're still not done, because a "sorting algorithm" that simply returns inputSize copies of the number 42 also satisfies this new spec. Suppose you notice this too, and think: "Aha! Every element in the input should also appear the same number of times in the output!" You're right -- and now, finally, your spec is actually complete. But you have no way to know that, so you will likely continue to wonder if there is some additional constraint out there that you haven't thought of yet... And this is all for one of the tidiest, most well-specified problems you could hope to encounter.

rramadass 11mo ago

Nada Amin's research mentioned in another thread is relevant here - https://news.ycombinator.com/item?id=46252034 https://news.ycombinator.com/item?id=46252034

seg_lol 11mo ago
Nada Amin isn't relevant to hacker news, she is 15 years ahead of grifting tech bros.
- rramadass 11mo ago
  Just to make sure that people don't get the wrong idea; Nada Amin's Harvard webpage states; I combine programming languages (PL) and artificial intelligence (AI), including large language models (LLMs), to create intelligent systems that are correct by construction. My current application domains include program and proof synthesis, and precision medicine. ... we look at combining Machine Learning and Programming Languages to enable the creation of neuro-symbolic systems that can move back and forth between learnable (neural) and interpretable (symbolic) representations of a system. She was a recipient of the Amazon Research Award 2024 for LLM-Augmented Semi-Automated Proofs for Interactive Verification - https://www.amazon.science/research-awards/program-updates/70-amazon-research-award-recipients-announced https://www.amazon.science/research-awards/program-updates/7...

Mikhail_Edoshin 11mo ago

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.

mchaver 11mo ago
I wasn't familiar with that book. For other users, I think the book they are referring to is Introduction to Algorithms A Creative Approach by Udi Manber.
skydhash 11mo ago
> What is utterly lacking is a formal notation for these computation-reasoning steps that is not tied to a specific programming language A formal notation for this is a programming language. Which is why everyone use pseudo code or something equivalent for a first pass thinking or for communication.
- Mikhail_Edoshin 11mo ago
  Not quite. It is in a way (very visible when we talk about invariants), but it is not, well, semantic. A good notation for those steps would allow me to make only the distinctions I care for and ignore the distinctions I do not care for. So, for example, if I want to describe the greatest common divisor algorithm, I would only focus on the arithmetic part and define the domain of the parameters as "positive integers" (or maybe "non-negative integers"). A real programming language has a different goal: the code must run and do something useful. So I am unlikely to be able to define the domain like that (won't be able to make important distinctions) and, at the same time, will likely have to attend to things I do not care about (will have to make unimportant distinctions). All this will cripple and obscure the logic. This is what happens now and as a result we have a different implementation of everything for every programming language.

victor_xuan 11mo ago

Formal specification only works once the system are in a relatively final shape. No body wants to pay that price when they are struggling with product market fit.

seg_lol 11mo ago
formal > typed > untyped > unsound > vibed
learningstud 11mo ago
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".

auggierose 11mo ago

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

pydry 11mo ago
Back when I first studied this 20 years ago the progenitors predicted it would get very popular one day. What actually happened was that some programming languages borrowed a few concepts and life carried on as before.
- auggierose 11mo ago
  I started with this 30 years ago, so yeah, I know the history :-) This time is different.
atq2119 11mo ago
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.

abrgr 11mo ago

Great article! > 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.

burnt-resistor 11mo ago

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. See also: seL4.

tug2024 11mo ago

[dead]