[HN Gopher] Ask HN: How to start with formal verification to fin...
       ___________________________________________________________________
        
       Ask HN: How to start with formal verification to find bugs
        
       We have a large codebase of a mostly functional code. Most of the
       code looks roughly like this                 def
       CalculateX(entity1: Type1, entity2: Type2):         when:         |
       entity1 is big -> 5         | entity1 is not big -> 6         |
       entity2 is round and entity1 purple -> 5       The conditions in
       the pattern matching block can get quite complex. The function
       might be defined for all instances if Type1 and Type2 but that is
       not required. Reasoning about a single function is reasonably easy.
       But we often find a bug where a function should be defined for all
       combinations of its input parameters but it is calling a function
       which is not defined for a requested case.  We do all kinds of
       things to ensure it is reasonably correct but it seems like it is
       never enough. We are toying around with an idea of formal
       verification of our code. I don't know from which angle to attack
       this issue first. I was playing with Z3 and Coq but they are like a
       distinct system. What is a typical workflow of how to verify a
       program? Do we have to rewrite it first in a formal verification
       system or is it possible to use some sort of source-to-source
       translation? Is there a way to make sure this translation is
       correct? How do I find a system that will be up for the task? How
       do I know it is computationally tractable?
        
       Author : tomas789
       Score  : 8 points
       Date   : 2021-10-03 20:51 UTC (2 hours ago)
        
       | throwaway81523 wrote:
       | > What is a typical workflow of how to verify a program?
       | 
       | If you mean an existing program, it is usually not done that way.
       | Instead, you develop the program and the proofs at the same time,
       | so they go hand and hand with each other.
       | 
       | If you just mean checking exhaustiveness of a case statement,
       | compilers can often do that for you.
        
       | manx wrote:
       | Which programming language are you using? It looks to me like you
       | need exhaustiveness checking for pattern matching. Languages like
       | Scala, OCaml, Purescript or Haskell support this out of the box.
       | 
       | Am I overlooking something?
        
       | triska wrote:
       | To reason about the program, one would first represent the entire
       | program in such a way that one can easily reason about it, for
       | example: about the conditions of these branches, and about
       | generalizations and relations of these conditions etc. For this,
       | you will benefit from a programming language that allows easy
       | reasoning about its own code by representing any given program's
       | abstract syntax tree as a data type of the language itself that
       | can be handled conveniently. The specific snippet you show seems
       | not to be of this kind, but it may be possible to reason about it
       | somehow in the language you are using.
       | 
       | In addition, you will benefit from a language that allows easy
       | meta-interpretation, because then you will be able to
       | automatically "go through" the program in various ways, and
       | really reason about the conditions, for example by asking: "Are
       | there any cases where such and such holds?", "Are there any cases
       | where a term may fall through the branches?" etc., and find it
       | out with a program that interprets the target program. You will
       | benefit from _abstract_ interpretation, where you  "go through"
       | the programs in a coarser sense. Dynamically typed languages tend
       | to allow easier meta-interpretation than statically typed
       | languages. As I see it, easier meta-interpretation is a major
       | attraction of dynamic type systems, arguably their most important
       | one.
       | 
       | Every indirection you take, such as a source-to-source
       | translation, will raise the question whether the transformation
       | of the program to a different form is itself correct and
       | preserves the properties you are interested in. Hence, it is
       | preferable to stay as close as possible to the actual target form
       | of the program in order to be certain that we are reasoning about
       | what is actually executed. In my experience, logic programming
       | languages like Prolog allow much easier reasoning about programs
       | than functional languages, also due to their implicit mechanisms
       | such as built-in search to systematically consider all possible
       | cases that can arise. A good way to answer such questions with
       | logic programming languages is to write a meta-interpreter that
       | interprets the program and keeps track of the properties you want
       | to reason about.
        
       ___________________________________________________________________
       (page generated 2021-10-03 23:01 UTC)