3 ms·

Formal verification is a bit like using a super high level strict/static/safe programming language (often in conjunction with a classic programming language pro

Formal verification is a bit like using a super high level strict/static/safe programming language (often in conjunction with a classic programming language providing the actual run-time description which is being formally checked). Think C# attributes or python decorators but where they take up 80% of the code and are a language onto themselves. It basically does all of the things you described in your list through automatic formal mathematical proofs, rather than relying on chance or on the programmer directly (obviously if you write a backdoor into a formal requirement it'll make it past the proving step). - No need to unit test specific cases when all the cases have been formally proven. - Formal proving methods typically work best (or at least most easily) on pure functions for the reasons you described. - No need to fuzz random values when the entire range has been formally proven. If you ever took a theoretical computer science where the teacher had you write the formal induction proof for a loop, it's like that, where every possible case must be covered mathematically. We've simply gotten the computer to deduce the proofs for us automatically. For example if there is a global integer that can be between 0 and 700, or the value 1000, then the formal verification system will make sure nothing in the program can write any other value to that memory. It will never increment or decrement when a 1000 is in there, it will never subtract 20 when a value less than 20 is in there, etc. Including by buffer overflows, or by pointer arithmetic in some random function, or by a runaway parsing algorithm. And then we do that for ever piece of memory, every subroutine call, and every possible input. And then we prove we covered every case and never violated our spec. And we can add implications to our spec. For example the only way a command to launch a missile can happen is if the launch missile function is called, no other function no matter the state of the program can cause it to happen. This can prove that there aren't exploits to a complex program that might cause unwanted behavior. Can you prove that sort of thing to me about your software? Like can you prove to me your software is unbreakable? This solution can (with a much smaller error rate than "well I tried 17 things and none of them worked." because it can say "I tried literally every possible thing."). It's a proactive solution. We are proving that it's mathematically impossible to break (engineering still being the weak point). That's an order of magnitude, if not more, better than what we have now.

gravypod 10y ago
So is it just writing a bunch of preconditions for a method? This was practice long before "formal methods" became a "trend". I still haven't had anyone show me how this works. If you, or anyone reading, could do the following I think it would really help all of us plebs who aren't much involved with academic computer science: can you write, from start to finish, a formally defined application documenting as you go and why you are doing it. For instance an F to C calculator. Could you make one of those and document your thoughts as you create it.
- elbows 10y ago
  It's more like writing preconditions and postconditions, and proving that the implementation of the function will always satisfying the postconditions. And then also proving that no other part of your program can call the function in a way that violates its preconditions. The proofs are checked automatically. I can't point you to a simple example. But you could check out the book "Software Foundations" (available for free at https://www.cis.upenn.edu/~bcpierce/sf/current/index.html https://www.cis.upenn.edu/~bcpierce/sf/current/index.html). If you have time to read the first few chapters it may clarify things.
  - gravypod 10y ago
    So then how is it any different from what most people already do? We already use assets liberally in development, specify everything in documentation, and then use linting systems to tell us if we violate our rules? This just sounds like another name used by people to sound like they are doing something that was already being done in the professional. Edit: I'll read through that book, thanks!
    - AstralStorm 10y ago
      In how much of the code are you actually applying those best practices? Are you verifying interactions between all modules? True formal verification checks everything, because anything unchecked shows up clearly as a baseless assumption (axiom).

gravypod 10y ago

So is it just writing a bunch of preconditions for a method? This was practice long before "formal methods" became a "trend". I still haven't had anyone show me how this works. If you, or anyone reading, could do the following I think it would really help all of us plebs who aren't much involved with academic computer science: can you write, from start to finish, a formally defined application documenting as you go and why you are doing it. For instance an F to C calculator. Could you make one of those and document your thoughts as you create it.

elbows 10y ago
It's more like writing preconditions and postconditions, and proving that the implementation of the function will always satisfying the postconditions. And then also proving that no other part of your program can call the function in a way that violates its preconditions. The proofs are checked automatically. I can't point you to a simple example. But you could check out the book "Software Foundations" (available for free at https://www.cis.upenn.edu/~bcpierce/sf/current/index.html https://www.cis.upenn.edu/~bcpierce/sf/current/index.html). If you have time to read the first few chapters it may clarify things.
- gravypod 10y ago
  So then how is it any different from what most people already do? We already use assets liberally in development, specify everything in documentation, and then use linting systems to tell us if we violate our rules? This just sounds like another name used by people to sound like they are doing something that was already being done in the professional. Edit: I'll read through that book, thanks!
  - AstralStorm 10y ago
    In how much of the code are you actually applying those best practices? Are you verifying interactions between all modules? True formal verification checks everything, because anything unchecked shows up clearly as a baseless assumption (axiom).