5 ms·

The specification is a lot smaller than the code, and so it's easier to read and manually verify that it's correct.

• fchollet 9y ago
  How is that the case in this specific example? It looks a lot harder to check for correctness.
  • dselsam 9y ago
    > The specification is a lot smaller than the code, and so it's easier to read and manually verify that it's correct. >> How is that the case in this specific example? It looks a lot harder to check for correctness. Author here. Here is the specification for the stochastic backpropagation algorithm: https://github.com/dselsam/certigrad/blob/master/src/certigrad/backprop_correct.lean#L13-L25 https://github.com/dselsam/certigrad/blob/master/src/certigr... The preconditions do not need to be inspected carefully because we prove that the models of interest satisfy them (example: https://github.com/dselsam/certigrad/blob/master/src/certigrad/aevb/grads_correct.lean#L20-L27 https://github.com/dselsam/certigrad/blob/master/src/certigr...) Here is the part of the specification that needs to be inspected carefully: https://github.com/dselsam/certigrad/blob/master/src/certigrad/backprop_correct.lean#L23-L25 https://github.com/dselsam/certigrad/blob/master/src/certigr... The syntax may seem strange to those unfamiliar with Lean, and a few of the functions involved may not be self-explanatory without reading their definitions, but the statement is conceptually simple: the stochastic backpropagation algorithm correctly computes unbiased estimates of the gradient of the expected loss. It is subjective, but I personally think that this specification is vastly easier to understand and to check for correctness than the actual implementation of the stochastic backpropagation algorithm.
• xgk 9y ago
  specification is a lot smaller than the code I doubt that this is the case in general. How can the (full) specification of a program be smaller than the program? This would mean we can always compress a program into a smaller program (after all a specification can be seen as another program -- alternatively a program can be seen as its own specification).
  • wizeman 9y ago
    It's not true for all cases, but it's true for most real-world cases, especially for typical combinations of specification tools and traditional (imperative) programming languages. A real-world program is usually more complex and intricate than a specification, often a lot more complex. This is usually done in the interest of optimization / performance, so that you program runs at least somewhat efficiently. A specification is usually a lot simpler, because typically you only need to express the simplest possible way to do or to describe something. Even if the specification ends up looking like a very simple, naive and horribly inefficient program to a typical programmer, it doesn't matter: it's not going to be executed, it's only going to be used to prove that your program behaves in the same way, even though your program can be arbitrarily more complex. Also, in your specification, sometimes you don't even need to express how to do something - you only need to express what the result looks like. For example, let's say you want to prove that a sorting algorithm is implemented correctly. You literally only have to specify "after running the function sort() on an array, the resulting array is sorted. A sorted array means that for any X and Y elements of the array, if the index of X is less than the index of Y, then the value of X is less than or equal to the value of Y". It's easy to see how that specifies correct sorting behavior, even though it doesn't even say how the sorting is supposed to be done. In contrast, the actual implementation of the sorting algorithm can be way more complex or difficult to see that is correct than that, especially if your program is written in a programming language prone to errors, with pointer manipulation and potential undefined behavior (such as C, for instance).
    • xgk 9y ago
      A specification is usually a lot simpler, because ... I used to think that too, but after verifying some algorithms, I have become sceptical of that belief. Instead I conjecture that on average the full specification of an algorithm is at best proportional in length to the algorithm itself. There are two main issues: - Most verification does not tackle the full specification, but rather some aspect. - Verification needs many intermediate specifications (e.g. induction hypotheses in proofs), which need to be accounted for. I'm happy to be convinced otherwise. prove that a sorting algorithm is I produced the full verification of Quicksort (probably the first), and I needed to produce a large amount of intermediate specifications for auxiliary lemmas. The full specification was much longer than the algorithm.