12 ms·

I think formal verification shines in areas where implementation is much more complex than the spec, like when you’re writing incomprehensible bit-level optimiz

by bkettle 9mo ago

I think formal verification shines in areas where implementation is much more complex than the spec, like when you’re writing incomprehensible bit-level optimizations in a cryptography implementation or compiler optimization phases. I’m not sure that most of us, day-to-day, write code (or have AI write code) that would benefit from formal verification, since to me it seems like high-level programming languages are already close to a specification language. I’m not sure how much easier to read a specification format that didn’t concern itself with implementation could be, especially when we currently use all kinds of frameworks and libraries that already abstract away implementation details. Sure, formal verification might give stronger guarantees about various levels of the stack, but I don’t think most of us care about having such strong guarantees now and I don’t think AI really introduces a need for new guarantees at that level.

socketcluster 9mo ago
Yes. I feel like people who are trying to push software verification have never worked on typical real-world software projects where the spec is like 100 pages long and still doesn't fully cover all the requirements and you still have to read between the lines and then requirements keep changing mid-way through the project... Implementing software to meet the spec takes a very long time and then you have to invest a lot of effort and deep thought to ensure that what you've produced fits within the spec so that the stakeholder will be satisfied. You need to be a mind-reader. It's hard even for a human who understands the full business, social and political context to disambiguate the meaning and intent of the spec; to try to express it mathematically would be an absolute nightmare... and extremely unwise. You would literally need some kind of super intelligence... And the amount of stream-of-thought tokens which would have to be generated to arrive at a correct, consistent, unambiguous formal spec is probably going to cost more than just hiring top software engineers to build the thing with 100% test coverage of all main cases and edge cases. Worst part is; after you do all the expensive work of formal verification; you end up proving the 'correctness' of a solution that the client doesn't want. The refactoring required will invalidate the entire proof from the beginning. We haven't even figured out the optimal way to formally architect software that is resilient to requirement changes; in fact, the industry is REALLY BAD at this. Almost nobody is even thinking about it. I am, but I sometimes feel like I may be the only person in the world who cares about designing optimal architectures to minimize line count and refactoring diff size. We'd have to solve this problem first before we even think about formal verification of 'most software'. Without a hypothetical super-intelligence which understands everything about the world; the risk of misinterpreting any given 'typical' requirement is almost 100%... And once we have such super-intelligence, we won't need formal verification because the super-intelligence will be able to code perfectly on the first attempt; no need to verify. And then there's the fact that most software can tolerate bugs... If operationally important big tech software which literally has millions of concurrent users can tolerate bugs, then most software can tolerate bugs.
- robot-wrangler 9mo ago
  The whole perspective of this argument is hard for me to grasp. I don't think anyone is suggesting that formal specs are an alternative to code, they are just an alternative to informal specs. And actually with AI the new spin is that they aren't even a mutually exclusive alternative. A bidirectional bridge that spans multiple representations from informal spec to semiformal spec to code seems ideal. You change the most relevant layer that you're interested in and then see updates propagating semi-automatically to other layers. I'd say the jury is out on whether this uses extra tokens or saves them, but a few things we do know. Chain of code works better than chain of thought, and chain-of-spec seems like a simple generalization. Markdown-based planning and task-tracking agent workflows work better than just YOLOing one-shot changes everywhere, and so intermediate representations are useful. It seems to me that you can't actually get rid of specs, right? So to shoot down the idea of productive cooperation between formal methods and LLM-style AI, one really must successfully argue that informal specs are inherently better than formal ones. Or even stronger: having only informal specs is better than having informal+formal.
  - socketcluster 9mo ago
    > A bidirectional bridge that spans multiple representations from informal spec Amusingly, what I'm hearing is literally "I have a bridge to sell you."
    - robot-wrangler 9mo ago
      There's always a bridge, dude. The only question is whether you want to buy one that's described as "a pretty good one, not too old, sold as is" or if you'd maybe prefer "spans X, holds Y, money back guarantee".
      - socketcluster 9mo ago
        I get it. Sometimes complexity is justified. I just don't feel this particular bridge is justified for 'mainstream software' which is what the article is about.
pron 9mo ago
> to me it seems like high-level programming languages are already close to a specification language They are not. The power of rich and succinct specification languages (like TLA+) comes from the ability to succinctly express things that cannot be efficiently computed, or at all. That is because a description of what a program does is necessarily at a higher level of abstraction than the program (i.e. there are many possible programs or even magical oracles that can do what a program does). To give a contrived example, let's say you want to state that a particular computation terminates. To do it in a clear and concise manner, you want to express the property of termination (and prove that the computation satisfies it), but that property is not, itself, computable. There are some ways around it, but as a rule, a specification language is more convenient when it can describe things that cannot be executed.
- goryDeets 9mo ago
  [dead]
- anon-3988 9mo ago
  > To give a contrived example, let's say you want to state that a particular computation terminates. To do it in a clear and concise manner, you want to express the property of termination (and prove that the computation satisfies it), but that property is not, itself, computable. There are some ways around it, but as a rule, a specification language is more convenient when it can describe things that cannot be executed. Do you really think it is going to be easier for the average developer to write a specification for their program that does not terminate vs Giving them a framework or a language that does not have for loop? Edit: If by formal verification you mean type checking. That I very much agree.
  - DennisP 9mo ago
    Maybe it's difficult for the average developer to write a formal specification, but the point of the article is that an AI can do it for them.
- nyrikki 9mo ago
  TLA+ is not a silver bullet, and like all temporal logic, has constraints. You really have to be able to reduce your models to: “at some point in the future, this will happen," or "it will always be true from now on” Have probabilistic outcomes? Or even floats [0] and it becomes challenging and strings are a mess. > Note there is not a float type. Floats have complex semantics that are extremely hard to represent. Usually you can abstract them out, but if you absolutely need floats then TLA+ is the wrong tool for the job. TLA+ works for the problems it is suitable for, try and extend past that and it simply fails. [0] https://learntla.com/core/operators.html https://learntla.com/core/operators.html
marcosdumay 9mo ago
There are many really important properties to enforce even on the most basic CRUD system. You can easily say things like "an anonymous user must never edit any data, except for the create account form", or "every user authorized to see a page must be listed on the admin page that lists what users can see a page". People don't verify those because it's hard, not for lack of value.
- bkettle 9mo ago
  Yeah fair enough. I can definitely see the value of property-based verification like this and agree that useful properties could be easy to express and that LLMs could feasibly verify them. I think full verification that an implementation implements an entire spec and nothing else seems much less practical even with AI, but of course that is just one flavor of verification.
- nextos 9mo ago
  Yes, in fact there is research on type systems to ensure information flow control, avoiding unauthorized data access by construction. Concrete Semantics [1] has a little example in §9.2. [1] http://concrete-semantics.org/concrete-semantics.pdf http://concrete-semantics.org/concrete-semantics.pdf
- rmah 9mo ago
  Yes, except their cookie preferences to comply with european law. Oh, and they should be able to change their theme from light/dark but only that. Oh and maybe this other thing. Except in situations where it would conflict with current sales promotions. Unless they're referred by a reseller partner. Unless it's during a demo, of course. etc, etc, etc. This is the sort of reality that a lot of developers in the business world deals with.
- Maxion 9mo ago
  Even > "an anonymous user must never edit any data, except for the create account form" Can quickly end up being > "an anonymous user must never edit any data, except for the create account form, and the feedback form" And a week later go to > "an anonymous user must never edit any data, except for the create account form, the feedback form, and the error submission form if they end up with a specific type of error" And then during christmas > > "an anonymous user must never edit any data, except for the create account form, the feedback form, and the error submission form if they end up with a specific type of error, and the order submission form if they visit it from this magic link. Those visiting from the magic link, should not be able to use the feedback form (marge had a bad experience last christmas going through feedbacks from the promotional campaign)"
giancarlostoro 9mo ago
> especially when we currently use all kinds of frameworks and libraries that already abstract away implementation details. This is my issue with algorithm driven interviewing. Even the creator of Homebrew got denied by Google because he couldn't do some binary sort or whatever it even was. He made a tool used by millions of developers, but apparently that's not good enough.
- StilesCrisis 9mo ago
  Google denies qualified people all the time. They would much rather reject a great hire than take a risk on accepting a mediocre one. I feel for him but it's just the nature of the beast. Not everyone will get in.
  - beautiful_zhixu 9mo ago
    This language sounds like chauvinism leading to closed-mindedness and efficiency. Of course there are tradeoffs to chauvinism, as Googlers possess the mind to notice. But a Googler does not need to worry about saying ambiguous truths without understanding their emotions to the masses, for they have Google behind them. With the might of the G stick, they can hammer out words with confidence.
  - ogogmad 9mo ago
    I've heard this before. Why do you think algorithm questions are effective for finding "good" hires? Are they?
    - giancarlostoro 9mo ago
      They certainly don't filter out toxic people who make others leave companies because they poison the well.
      - ogogmad 9mo ago
        I have a suspicion that "good candidate" is being gerrymandered. What might have been "good" in 1990 might have become irrelevant in 2000+ or perhaps detrimental. I say that as someone who is actually good at algorithm questions himself. I think GP, as well as other Google defenders, are parroting pseudo-science.
amw-zero 9mo ago
Compare the spec with the application here: https://concerningquality.com/model-based-testing/ https://concerningquality.com/model-based-testing/ I think we've become used to the complexity in typical web applications, but there's a difference between familiar and simple (simple vs. easy, as it were). The behavior of most business software can be very simply expressed using simple data structures (sets, lists, maps) and simple logic. No matter how much we simply it, via frameworks and libraries or whatever have you, things like serialization, persistence, asynchrony, concurrency, and performance end up complicating the implementation. Comparing this against a simpler spec is quite nice in practice - and a huge benefit is now you can consult a simple in-memory spec vs. worrying about distributed system deployments.
UltraSane 9mo ago
AWS has said that having formal verification of code lets them be more aggressive in optimization while being confidant it still adheres to the spec. They claim they were able to double the speed of IAM API auth code this way.

by bkettle 9mo ago

socketcluster 9mo ago

Yes. I feel like people who are trying to push software verification have never worked on typical real-world software projects where the spec is like 100 pages long and still doesn't fully cover all the requirements and you still have to read between the lines and then requirements keep changing mid-way through the project... Implementing software to meet the spec takes a very long time and then you have to invest a lot of effort and deep thought to ensure that what you've produced fits within the spec so that the stakeholder will be satisfied. You need to be a mind-reader. It's hard even for a human who understands the full business, social and political context to disambiguate the meaning and intent of the spec; to try to express it mathematically would be an absolute nightmare... and extremely unwise. You would literally need some kind of super intelligence... And the amount of stream-of-thought tokens which would have to be generated to arrive at a correct, consistent, unambiguous formal spec is probably going to cost more than just hiring top software engineers to build the thing with 100% test coverage of all main cases and edge cases. Worst part is; after you do all the expensive work of formal verification; you end up proving the 'correctness' of a solution that the client doesn't want. The refactoring required will invalidate the entire proof from the beginning. We haven't even figured out the optimal way to formally architect software that is resilient to requirement changes; in fact, the industry is REALLY BAD at this. Almost nobody is even thinking about it. I am, but I sometimes feel like I may be the only person in the world who cares about designing optimal architectures to minimize line count and refactoring diff size. We'd have to solve this problem first before we even think about formal verification of 'most software'. Without a hypothetical super-intelligence which understands everything about the world; the risk of misinterpreting any given 'typical' requirement is almost 100%... And once we have such super-intelligence, we won't need formal verification because the super-intelligence will be able to code perfectly on the first attempt; no need to verify. And then there's the fact that most software can tolerate bugs... If operationally important big tech software which literally has millions of concurrent users can tolerate bugs, then most software can tolerate bugs.

robot-wrangler 9mo ago
The whole perspective of this argument is hard for me to grasp. I don't think anyone is suggesting that formal specs are an alternative to code, they are just an alternative to informal specs. And actually with AI the new spin is that they aren't even a mutually exclusive alternative. A bidirectional bridge that spans multiple representations from informal spec to semiformal spec to code seems ideal. You change the most relevant layer that you're interested in and then see updates propagating semi-automatically to other layers. I'd say the jury is out on whether this uses extra tokens or saves them, but a few things we do know. Chain of code works better than chain of thought, and chain-of-spec seems like a simple generalization. Markdown-based planning and task-tracking agent workflows work better than just YOLOing one-shot changes everywhere, and so intermediate representations are useful. It seems to me that you can't actually get rid of specs, right? So to shoot down the idea of productive cooperation between formal methods and LLM-style AI, one really must successfully argue that informal specs are inherently better than formal ones. Or even stronger: having only informal specs is better than having informal+formal.
- socketcluster 9mo ago
  > A bidirectional bridge that spans multiple representations from informal spec Amusingly, what I'm hearing is literally "I have a bridge to sell you."
  - robot-wrangler 9mo ago
    There's always a bridge, dude. The only question is whether you want to buy one that's described as "a pretty good one, not too old, sold as is" or if you'd maybe prefer "spans X, holds Y, money back guarantee".
    - socketcluster 9mo ago
      I get it. Sometimes complexity is justified. I just don't feel this particular bridge is justified for 'mainstream software' which is what the article is about.

pron 9mo ago

> to me it seems like high-level programming languages are already close to a specification language They are not. The power of rich and succinct specification languages (like TLA+) comes from the ability to succinctly express things that cannot be efficiently computed, or at all. That is because a description of what a program does is necessarily at a higher level of abstraction than the program (i.e. there are many possible programs or even magical oracles that can do what a program does). To give a contrived example, let's say you want to state that a particular computation terminates. To do it in a clear and concise manner, you want to express the property of termination (and prove that the computation satisfies it), but that property is not, itself, computable. There are some ways around it, but as a rule, a specification language is more convenient when it can describe things that cannot be executed.

goryDeets 9mo ago
[dead]
anon-3988 9mo ago
> To give a contrived example, let's say you want to state that a particular computation terminates. To do it in a clear and concise manner, you want to express the property of termination (and prove that the computation satisfies it), but that property is not, itself, computable. There are some ways around it, but as a rule, a specification language is more convenient when it can describe things that cannot be executed. Do you really think it is going to be easier for the average developer to write a specification for their program that does not terminate vs Giving them a framework or a language that does not have for loop? Edit: If by formal verification you mean type checking. That I very much agree.
- DennisP 9mo ago
  Maybe it's difficult for the average developer to write a formal specification, but the point of the article is that an AI can do it for them.
nyrikki 9mo ago
TLA+ is not a silver bullet, and like all temporal logic, has constraints. You really have to be able to reduce your models to: “at some point in the future, this will happen," or "it will always be true from now on” Have probabilistic outcomes? Or even floats [0] and it becomes challenging and strings are a mess. > Note there is not a float type. Floats have complex semantics that are extremely hard to represent. Usually you can abstract them out, but if you absolutely need floats then TLA+ is the wrong tool for the job. TLA+ works for the problems it is suitable for, try and extend past that and it simply fails. [0] https://learntla.com/core/operators.html https://learntla.com/core/operators.html

marcosdumay 9mo ago

There are many really important properties to enforce even on the most basic CRUD system. You can easily say things like "an anonymous user must never edit any data, except for the create account form", or "every user authorized to see a page must be listed on the admin page that lists what users can see a page". People don't verify those because it's hard, not for lack of value.

bkettle 9mo ago
Yeah fair enough. I can definitely see the value of property-based verification like this and agree that useful properties could be easy to express and that LLMs could feasibly verify them. I think full verification that an implementation implements an entire spec and nothing else seems much less practical even with AI, but of course that is just one flavor of verification.
nextos 9mo ago
Yes, in fact there is research on type systems to ensure information flow control, avoiding unauthorized data access by construction. Concrete Semantics [1] has a little example in §9.2. [1] http://concrete-semantics.org/concrete-semantics.pdf http://concrete-semantics.org/concrete-semantics.pdf
rmah 9mo ago
Yes, except their cookie preferences to comply with european law. Oh, and they should be able to change their theme from light/dark but only that. Oh and maybe this other thing. Except in situations where it would conflict with current sales promotions. Unless they're referred by a reseller partner. Unless it's during a demo, of course. etc, etc, etc. This is the sort of reality that a lot of developers in the business world deals with.
Maxion 9mo ago
Even > "an anonymous user must never edit any data, except for the create account form" Can quickly end up being > "an anonymous user must never edit any data, except for the create account form, and the feedback form" And a week later go to > "an anonymous user must never edit any data, except for the create account form, the feedback form, and the error submission form if they end up with a specific type of error" And then during christmas > > "an anonymous user must never edit any data, except for the create account form, the feedback form, and the error submission form if they end up with a specific type of error, and the order submission form if they visit it from this magic link. Those visiting from the magic link, should not be able to use the feedback form (marge had a bad experience last christmas going through feedbacks from the promotional campaign)"

giancarlostoro 9mo ago

> especially when we currently use all kinds of frameworks and libraries that already abstract away implementation details. This is my issue with algorithm driven interviewing. Even the creator of Homebrew got denied by Google because he couldn't do some binary sort or whatever it even was. He made a tool used by millions of developers, but apparently that's not good enough.

StilesCrisis 9mo ago
Google denies qualified people all the time. They would much rather reject a great hire than take a risk on accepting a mediocre one. I feel for him but it's just the nature of the beast. Not everyone will get in.
- beautiful_zhixu 9mo ago
  This language sounds like chauvinism leading to closed-mindedness and efficiency. Of course there are tradeoffs to chauvinism, as Googlers possess the mind to notice. But a Googler does not need to worry about saying ambiguous truths without understanding their emotions to the masses, for they have Google behind them. With the might of the G stick, they can hammer out words with confidence.
- ogogmad 9mo ago
  I've heard this before. Why do you think algorithm questions are effective for finding "good" hires? Are they?
  - giancarlostoro 9mo ago
    They certainly don't filter out toxic people who make others leave companies because they poison the well.
    - ogogmad 9mo ago
      I have a suspicion that "good candidate" is being gerrymandered. What might have been "good" in 1990 might have become irrelevant in 2000+ or perhaps detrimental. I say that as someone who is actually good at algorithm questions himself. I think GP, as well as other Google defenders, are parroting pseudo-science.

amw-zero 9mo ago

Compare the spec with the application here: https://concerningquality.com/model-based-testing/ https://concerningquality.com/model-based-testing/ I think we've become used to the complexity in typical web applications, but there's a difference between familiar and simple (simple vs. easy, as it were). The behavior of most business software can be very simply expressed using simple data structures (sets, lists, maps) and simple logic. No matter how much we simply it, via frameworks and libraries or whatever have you, things like serialization, persistence, asynchrony, concurrency, and performance end up complicating the implementation. Comparing this against a simpler spec is quite nice in practice - and a huge benefit is now you can consult a simple in-memory spec vs. worrying about distributed system deployments.

UltraSane 9mo ago

AWS has said that having formal verification of code lets them be more aggressive in optimization while being confidant it still adheres to the spec. They claim they were able to double the speed of IAM API auth code this way.