3 ms·

You Already Know Formal Methods

87 points by azhenley 5y ago

carapace 5y ago
I like to say "You're already using informal formal methods" when attempting to get this point across. The typical argument against Formal Methods is based on cost, to which the reply could be "Well what's the cost of broken code?" I'm glad the tools and languages to do FM are getting more common and familiar.
- cryptica 5y ago
  IMO, poor choice of logic is more common and more harmful than incorrect logic. It's not that the algorithm is incorrect; it's that the wrong algorithm or the wrong abstraction were chosen to solve particular problems. Sometimes the whole architecture of a system encompassing millions of lines of code is wrong in a fundamental way even if every part of it is entirely logically correct. You can't narrow down the problem to any specific part of the code. The problem is architectural; the design of the system prevents it from meeting scalability requirements for example or it doesn't handle changing requirements very well; the interfaces are too rigid... Not well chosen.
  - chriswarbo 5y ago
    That distinction is usually captured as validation versus verification. Formal methods can verify that an implementation satisfies its specification (i.e. that we got what we asked for). To know whether the specification is reasonable/appropriate/etc. requires we validate it against our needs (i.e. that we're asking for the right thing).
    - cryptica 5y ago
      Makes sense. In that context, I think that verification is nowhere near as challenging as validation when it comes to coding. Verification is definitely a big concern for junior developers who don't know how to write good tests, however, beyond a certain level of expertise, the big challenge becomes validation. If written properly, tests do a pretty good job at verification. Formal proofs only take care of rare edge cases (since tests can never be exhaustive), but many times, it's possible (and recommended) to write code in a way to minimize such rare edge cases anyway.
      - chriswarbo 5y ago
        I agree that validation is important (e.g. avoid optimising things which shouldn't exist https://youtu.be/t705r8ICkRw?t=1022 https://youtu.be/t705r8ICkRw?t=1022 ). It's all about bang-for-buck: a formal proof can give me lots of confidence about some aspect of a system, but might take a long time and have a maintenance burden; if that time and maintenance could give me more confidence when used to write masses of tests instead, then it's probably better to go with the tests. My go-to approach is property-based testing, since that can exercise edge-cases more effectively than hand-picked examples, whilst taking about the same amount of effort to write. A couple of things in favour of "proper" formal methods (in niche circumstances): - Sometimes the effort calculation tips in favour of a formal methods; e.g. reliably testing concurrent, distributed systems is notoriously hard, and might require even more effort than doing some proofs instead. - Proof objects themselves, and the act of writing them, can be useful for understanding a domain or system, and why certain things are/aren't true. This doesn't apply so much for "yes/no" solvers, like SAT/SMT/resolution/etc. but is often the case for "interactive" systems like Coq/Agda.
- throwaway81523 5y ago
  Pierce's very influential book "Types and Programming Languages" (TAPL) makes the case that type systems are "lightweight formal methods".
nivertech 5y ago
Decision Tables[1] is probably the simplest formal method, i.e. instead of writing imperative nested if and switch/case statements, your provide a declarative solution. But IMO the most useful formal method in Software Engineering is modeling your code as an FSMs, for example using StateCharts UML notation [2,3]. That way even junior developers can reason about complex realtime systems. Next close come Algebraic Type Systems, but they're usually not available in mainstream PLs. Unfortunately Formal Specification/Verification tools like TLA+, Alloy, etc. are less practical for most real life projects. -- [1] https://en.wikipedia.org/wiki/Decision_table https://en.wikipedia.org/wiki/Decision_table [2] https://en.wikipedia.org/wiki/UML_state_machine https://en.wikipedia.org/wiki/UML_state_machine [3] https://en.wikipedia.org/wiki/State_diagram#Harel_statechart https://en.wikipedia.org/wiki/State_diagram#Harel_statechart
- brenainn 5y ago
  State machines are handy, and along with modelling they can be implemented directly. A simple implementation is you define the possible states for your application, or module or whatever, and the valid transitions from state to state. You assign the new state when the state should transition, and this assignment is wrapped by some simple check that the transition is valid. If not, throw an error, or handle it, etc. The state path can also be logged to aid with debugging. I've found it invaluable in building web apps, finding odd things not caught in traditional testing e.g. like cases of trying to transition from the current state to the same state.
- rowanG077 5y ago
  What are Algebraic Type Systems? Google only gives me the run of the mill algabraic data types.
  - nivertech 5y ago
    I mean type systems used in ML family PLs. They're a static type systems based on algebraic data types. https://en.wikipedia.org/wiki/Algebraic_data_type https://en.wikipedia.org/wiki/Algebraic_data_type
- 5y ago
vbtemp 5y ago
Galois is a bit of an interesting and unique company I've followed for some time. Really interesting work in trusted and formally verifiable systems. But I can't shake the sense that there's a lot of bark but little "bite" -- Many of the utilities they release as open source seem half-baked; requests for more information (not even tech support) went unanswered; got rejected email notifications for listed email addresses. I've been wanting to incorporate their tech, but often feel their goal is to mostly to satisfy DARPA program managers, rather than be used in-the-field.
- jldodds 5y ago
  I'm sorry you've gotten that impression. We do have some things we'd be interested in getting more users for, but much of what we build is prototypes. If you're interested I'd love to talk.

87 points by azhenley 5y ago

I like to say "You're already using informal formal methods" when attempting to get this point across. The typical argument against Formal Methods is based on cost, to which the reply could be "Well what's the cost of broken code?" I'm glad the tools and languages to do FM are getting more common and familiar.

cryptica 5y ago
IMO, poor choice of logic is more common and more harmful than incorrect logic. It's not that the algorithm is incorrect; it's that the wrong algorithm or the wrong abstraction were chosen to solve particular problems. Sometimes the whole architecture of a system encompassing millions of lines of code is wrong in a fundamental way even if every part of it is entirely logically correct. You can't narrow down the problem to any specific part of the code. The problem is architectural; the design of the system prevents it from meeting scalability requirements for example or it doesn't handle changing requirements very well; the interfaces are too rigid... Not well chosen.
- chriswarbo 5y ago
  That distinction is usually captured as validation versus verification. Formal methods can verify that an implementation satisfies its specification (i.e. that we got what we asked for). To know whether the specification is reasonable/appropriate/etc. requires we validate it against our needs (i.e. that we're asking for the right thing).
  - cryptica 5y ago
    Makes sense. In that context, I think that verification is nowhere near as challenging as validation when it comes to coding. Verification is definitely a big concern for junior developers who don't know how to write good tests, however, beyond a certain level of expertise, the big challenge becomes validation. If written properly, tests do a pretty good job at verification. Formal proofs only take care of rare edge cases (since tests can never be exhaustive), but many times, it's possible (and recommended) to write code in a way to minimize such rare edge cases anyway.
    - chriswarbo 5y ago
      I agree that validation is important (e.g. avoid optimising things which shouldn't exist https://youtu.be/t705r8ICkRw?t=1022 https://youtu.be/t705r8ICkRw?t=1022 ). It's all about bang-for-buck: a formal proof can give me lots of confidence about some aspect of a system, but might take a long time and have a maintenance burden; if that time and maintenance could give me more confidence when used to write masses of tests instead, then it's probably better to go with the tests. My go-to approach is property-based testing, since that can exercise edge-cases more effectively than hand-picked examples, whilst taking about the same amount of effort to write. A couple of things in favour of "proper" formal methods (in niche circumstances): - Sometimes the effort calculation tips in favour of a formal methods; e.g. reliably testing concurrent, distributed systems is notoriously hard, and might require even more effort than doing some proofs instead. - Proof objects themselves, and the act of writing them, can be useful for understanding a domain or system, and why certain things are/aren't true. This doesn't apply so much for "yes/no" solvers, like SAT/SMT/resolution/etc. but is often the case for "interactive" systems like Coq/Agda.
throwaway81523 5y ago
Pierce's very influential book "Types and Programming Languages" (TAPL) makes the case that type systems are "lightweight formal methods".

nivertech 5y ago

Decision Tables[1] is probably the simplest formal method, i.e. instead of writing imperative nested if and switch/case statements, your provide a declarative solution. But IMO the most useful formal method in Software Engineering is modeling your code as an FSMs, for example using StateCharts UML notation [2,3]. That way even junior developers can reason about complex realtime systems. Next close come Algebraic Type Systems, but they're usually not available in mainstream PLs. Unfortunately Formal Specification/Verification tools like TLA+, Alloy, etc. are less practical for most real life projects. -- [1] https://en.wikipedia.org/wiki/Decision_table https://en.wikipedia.org/wiki/Decision_table [2] https://en.wikipedia.org/wiki/UML_state_machine https://en.wikipedia.org/wiki/UML_state_machine [3] https://en.wikipedia.org/wiki/State_diagram#Harel_statechart https://en.wikipedia.org/wiki/State_diagram#Harel_statechart

brenainn 5y ago
State machines are handy, and along with modelling they can be implemented directly. A simple implementation is you define the possible states for your application, or module or whatever, and the valid transitions from state to state. You assign the new state when the state should transition, and this assignment is wrapped by some simple check that the transition is valid. If not, throw an error, or handle it, etc. The state path can also be logged to aid with debugging. I've found it invaluable in building web apps, finding odd things not caught in traditional testing e.g. like cases of trying to transition from the current state to the same state.
rowanG077 5y ago
What are Algebraic Type Systems? Google only gives me the run of the mill algabraic data types.
- nivertech 5y ago
  I mean type systems used in ML family PLs. They're a static type systems based on algebraic data types. https://en.wikipedia.org/wiki/Algebraic_data_type https://en.wikipedia.org/wiki/Algebraic_data_type
5y ago

vbtemp 5y ago

Galois is a bit of an interesting and unique company I've followed for some time. Really interesting work in trusted and formally verifiable systems. But I can't shake the sense that there's a lot of bark but little "bite" -- Many of the utilities they release as open source seem half-baked; requests for more information (not even tech support) went unanswered; got rejected email notifications for listed email addresses. I've been wanting to incorporate their tech, but often feel their goal is to mostly to satisfy DARPA program managers, rather than be used in-the-field.

jldodds 5y ago
I'm sorry you've gotten that impression. We do have some things we'd be interested in getting more users for, but much of what we build is prototypes. If you're interested I'd love to talk.