4 ms·

As the article mentions, formal verification techniques are primarily used today for two things: - Creating secure "core" code -- library functions and kernels

As the article mentions, formal verification techniques are primarily used today for two things: - Creating secure "core" code -- library functions and kernels and stuff, where the things they're supposed to do are very well-defined. - Verifying specific, narrowly defined properties, like how Rust's borrow checker guarantees that your program doesn't try to write to the same value from two different threads at once. I'm not sure formal techniques will be as useful when expanded to other areas. Most of the bugs I encounter day-to-day happen because the programmer had the wrong goal in mind -- if you asked them to create a formal proof that their code worked, they would be able to do that, but it would be a proof that their function did a thing which was not actually the thing we wanted. (Similarly to, e.g., unit tests that do not actually test anything because they're just line-by-line reproductions of the original code but with every function call mocked out.) Has anyone successfully applied proof techniques to reduce defects in UI development, "business logic", or similarly fuzzy disciplines?

er4hn 4y ago
I would love to see a fuzzer applied to business logic. It should take design requests from PMs and execucritters and ask pointed questions about edge cases.
- Transfinity 4y ago
  I love this idea. I bet you could get surprisingly useful results just using a language model like GPT-3.
johnbender 4y ago
I think this sharply discounts the value of the step before the proof which is writing the specification in a formal language/logic. This often surfaces these misunderstandings before a proof is even necessary. That doesn’t guarantee that the spec will be the right one (as you say) but it’s astounding how often just writing it down formally improves the implementation through rigorous thought.
- pydry 4y ago
  I've only done a bit of formal verification but I'd estimate that writing that spec was 7-10x harder than writing the actual program and was more complicated than the code. In the end I had lower confidence that the spec lacked bugs than the program. This was after expending a huge amount of effort on a pretty tiny program. I dont think this was a tooling thing. I think it spoke to the fundamental limits of formal verification. I think it'll always remain kinda niche.
  - johnbender 4y ago
    I think this depends on the spec language and the target system. I’ve never encountered a spec more complicated than the program as the goal is always abstraction but I don’t mean to discount your experiences and complexity is affected by tooling familiarity and quality. Separately the spec can often have its own properties which can be verified as a means to interrogate its correctness. For example state machines as spec, temporal logic properties and model checking where the state machine is the abstraction for a concrete system. Worth noting that proving state machines are an abstraction of a concrete system is a going research concern though.
  - danielvf 4y ago
    I've used formal verification in anger, as well as working with a vendor to formaly verify some critical code for us. This rings very true. It is extraordinarily difficult to write correct rules. It ends up being the same problem as wishing against an evil genie. Most rules that you come up with at first end up having a class of obvious exceptions in the real world, which the verifier finds, and then even more unobvious exceptions, and soon your logic around the exceptions to the rules become at least as complicated as the code you are attempting to verify. And in this any wrong assumptions that falsely allow bad behavior are not caught or flagged because they pass. Even giving perfect proving software, it's still a far harder challenge to write rules than to write code. And current software is still far from perfect - you are likely to spend a lot of your rules time fighting with your prover.
- lelanthran 4y ago
  > I think this sharply discounts the value of the step before the proof which is writing the specification in a formal language/logic. If that was at all achievable, we'd have a compiler that took the "specification in a formal language/logic" and emitted native code/applications/programs. We'd then call the "specification in a formal language/logic" a programming language. Sure, there are a lot of formal languages for specifying logic with checkers that ensure no bugs in the input specification exist, but AFAIK none of them are useful enough to emit programs. Needing a human to translate one formal language (the formal spec) into another formal language is pointless and useless, because then the human may as well just translate human language specification into formal language.
deleted 4y ago
[deleted]

er4hn 4y ago

I would love to see a fuzzer applied to business logic. It should take design requests from PMs and execucritters and ask pointed questions about edge cases.

Transfinity 4y ago
I love this idea. I bet you could get surprisingly useful results just using a language model like GPT-3.

johnbender 4y ago

I think this sharply discounts the value of the step before the proof which is writing the specification in a formal language/logic. This often surfaces these misunderstandings before a proof is even necessary. That doesn’t guarantee that the spec will be the right one (as you say) but it’s astounding how often just writing it down formally improves the implementation through rigorous thought.

pydry 4y ago
I've only done a bit of formal verification but I'd estimate that writing that spec was 7-10x harder than writing the actual program and was more complicated than the code. In the end I had lower confidence that the spec lacked bugs than the program. This was after expending a huge amount of effort on a pretty tiny program. I dont think this was a tooling thing. I think it spoke to the fundamental limits of formal verification. I think it'll always remain kinda niche.
- johnbender 4y ago
  I think this depends on the spec language and the target system. I’ve never encountered a spec more complicated than the program as the goal is always abstraction but I don’t mean to discount your experiences and complexity is affected by tooling familiarity and quality. Separately the spec can often have its own properties which can be verified as a means to interrogate its correctness. For example state machines as spec, temporal logic properties and model checking where the state machine is the abstraction for a concrete system. Worth noting that proving state machines are an abstraction of a concrete system is a going research concern though.
- danielvf 4y ago
  I've used formal verification in anger, as well as working with a vendor to formaly verify some critical code for us. This rings very true. It is extraordinarily difficult to write correct rules. It ends up being the same problem as wishing against an evil genie. Most rules that you come up with at first end up having a class of obvious exceptions in the real world, which the verifier finds, and then even more unobvious exceptions, and soon your logic around the exceptions to the rules become at least as complicated as the code you are attempting to verify. And in this any wrong assumptions that falsely allow bad behavior are not caught or flagged because they pass. Even giving perfect proving software, it's still a far harder challenge to write rules than to write code. And current software is still far from perfect - you are likely to spend a lot of your rules time fighting with your prover.
lelanthran 4y ago
> I think this sharply discounts the value of the step before the proof which is writing the specification in a formal language/logic. If that was at all achievable, we'd have a compiler that took the "specification in a formal language/logic" and emitted native code/applications/programs. We'd then call the "specification in a formal language/logic" a programming language. Sure, there are a lot of formal languages for specifying logic with checkers that ensure no bugs in the input specification exist, but AFAIK none of them are useful enough to emit programs. Needing a human to translate one formal language (the formal spec) into another formal language is pointless and useless, because then the human may as well just translate human language specification into formal language.

deleted 4y ago

[deleted]