3 ms·

A Formal Method means to create a Formal System and construct a formal proof. https://en.wikipedia.org/wiki/Formal_system https://en.wikipedia.org/wiki/Formal_

A Formal Method means to create a Formal System and construct a formal proof. https://en.wikipedia.org/wiki/Formal_system https://en.wikipedia.org/wiki/Formal_system As a small example of using Hoare Logic, which takes every single command (aka line of code) in your program and turns it in to a Hoare Triple. A Hoare Triple looks like {precondition} command {postcondition}. As an example let's prove the output is not 476. int numb; ..... numb = numb * 2; numb = numb + 1; print numb For print numb to print 476 we have the precondition that numb must be 476. {numb = 476} print numb {We don't care what happens after you print} If numb is 476 on the line above then the line before this one must have a post condition identical to this line's precondition. {} numb = numb + 1; {numb = 476} For this line to be true it must have a precondition that numb = 475 so {numb = 475} numb + 1; {numb = 476} Again we chain this line's precondition to the previous line's post condition: {} numb = numb * 2; {numb = 475} Given that numb is defined as an integer there is no possible precondition capable of making this post condition true. We have formally proven this program is incapable of printing 476. Further since the stuff in the brackets can be as complex as we like we could have proven this program is incapable of printing even numbers. https://en.wikipedia.org/wiki/Hoare_logic https://en.wikipedia.org/wiki/Hoare_logic

gravypod 10y ago
Doesn't that rely on, often incorrect, assumptions of underlying hardware? Doesn't this change based on the environment that the system is going to be put in? There are things people are saying are "guaranteed" about formal systems that just aren't true. To have a formal system actually be "correct" it needs to have never touched "incorrect" software or hardware. This contains, but is not limited to, a "correct" compiler and hardware implementation. This is, I'd say, often not the case.
- vilhelm_s 10y ago
  Right, whenever you try to use mathematics/logic to reason about the real world, you risk that some of your assumptions may be wrong. Every formally verified project will have some set of trusted assumptions. But hopefully this can still dramatically reduce software vulnerabilities---for example, systems more often fail because of bugs in the program logic than bugs in the x86 processor, so assuming a specification for the hardware and proving the program correct with respect to that should still be helpful. (As an aside, hardware and compilers are actually comparatively tractable things to verify--the specifications are well-defined, and they are used by lots of clients so the effort to verify them pays off better. I think in the future, we are more likely to have unproven application programs running on top of proven compilers & hardware than the opposite.)

gravypod 10y ago

Doesn't that rely on, often incorrect, assumptions of underlying hardware? Doesn't this change based on the environment that the system is going to be put in? There are things people are saying are "guaranteed" about formal systems that just aren't true. To have a formal system actually be "correct" it needs to have never touched "incorrect" software or hardware. This contains, but is not limited to, a "correct" compiler and hardware implementation. This is, I'd say, often not the case.

vilhelm_s 10y ago
Right, whenever you try to use mathematics/logic to reason about the real world, you risk that some of your assumptions may be wrong. Every formally verified project will have some set of trusted assumptions. But hopefully this can still dramatically reduce software vulnerabilities---for example, systems more often fail because of bugs in the program logic than bugs in the x86 processor, so assuming a specification for the hardware and proving the program correct with respect to that should still be helpful. (As an aside, hardware and compilers are actually comparatively tractable things to verify--the specifications are well-defined, and they are used by lots of clients so the effort to verify them pays off better. I think in the future, we are more likely to have unproven application programs running on top of proven compilers & hardware than the opposite.)