4 ms·

Seems like they are using a narrow definition of "mathematically provable" -- they only thing that appears to be proven is that "all memory access is mathematic

by lwb 7y ago

Seems like they are using a narrow definition of "mathematically provable" -- they only thing that appears to be proven is that "all memory access is mathematically proven to be defined". Which just seems like a fancy way of achieving the same thing as a type checker? Either way, cool project, but is there anything else that ZZ can prove?

augusto-moura 7y ago
In the README there's a example of proving a simple state machine open > read > close [1] Just read the docs™ [1] https://github.com/aep/zz#theory https://github.com/aep/zz#theory
- lwb 7y ago
  Ah ok, not sure how I missed that. That still seems to be within the realm of a type system, no? Or would you consider type systems a subset of mathematically provable systems?
  - ludamad 7y ago
    Dependent type systems certainly are!
  - augusto-moura 7y ago
    Well Type Theory is actually one of the definitions of mathematics and computation[1]. Wikipedia gives a basic definition of it [2][3] [1] https://en.wikipedia.org/wiki/Typed_lambda_calculus https://en.wikipedia.org/wiki/Typed_lambda_calculus [2] https://en.wikipedia.org/wiki/Type_theory https://en.wikipedia.org/wiki/Type_theory [3] https://en.wikipedia.org/wiki/Foundations_of_mathematics https://en.wikipedia.org/wiki/Foundations_of_mathematics
- MaxBarraclough 7y ago
  So it has typestates. (I recommend anyone [0] and its HN thread [1] for detail.) I think that's a great language feature for helping to avoid bugs, especially the kind that often happen in C, but I don't imagine it's anywhere close to proving whole-program correctness, is it? For the curious, here's an official example in the SPARK language, that gives a proven-correct sort function. (A complete proof of correct program behaviour, not just absence of undefined behaviour). As you can see, proving correctness is a challenge that permeates every inch of the code. [2][3] Microsoft's Dafny language is similar. [4] [0] https://yoric.github.io/post/rust-typestate/ https://yoric.github.io/post/rust-typestate/ [1] https://news.ycombinator.com/item?id=21413174 https://news.ycombinator.com/item?id=21413174 [2] https://github.com/AdaCore/spark2014/blob/76e08d279c/docs/ug/gnatprove_by_example/examples/sort.ads https://github.com/AdaCore/spark2014/blob/76e08d279c/docs/ug... [3] https://github.com/AdaCore/spark2014/blob/76e08d279c/docs/ug/gnatprove_by_example/examples/sort.adb https://github.com/AdaCore/spark2014/blob/76e08d279c/docs/ug... [4] https://en.wikipedia.org/wiki/Dafny#Imperative_features https://en.wikipedia.org/wiki/Dafny#Imperative_features
  - augusto-moura 7y ago
    I imagine that whole-program correctness can be represented, but is not enforced in the case of ZZ. Developers are not obligated to declare typesets for their own code or can rely on other libraries being fully typed
    - MaxBarraclough 7y ago
      > not enforced in the case of ZZ I don't think it's really even possible for a language to force the programmer to give a proper formal specification. We may want the formal spec to grant some leeway, i.e. not to specify the exact output/behaviour, but instead to express certain important constraints. For instance, we may not care which traffic-light turns green first, so long as the system preserves the important properties about safety and liveness. If we wish to support such flexibility, we can't stop the programmer from expressing all output states are valid. If we don't wish to support such flexibility, what we're really doing is comparing against a reference implementation.
      - zozbot234 7y ago
        > I don't think it's really even possible for a language to force the programmer to give a proper formal specification. The language, probably not. The standard library can certainly require detailed-enough formal preconditions to make its code defect-free, meaning that any remaining bugs can then be directly traced to the programmer's code.
        MaxBarraclough 7y ago
        You mean that, for instance, a standard-library generic sort function, might require that your comparator function behave correctly when the arguments are reversed? That's an interesting idea. Like Java interfaces, but with formal contracts. I doubt that putting these contracts into the standard-library would give you good proof-coverage though.
    - a3p 7y ago
      that is correct. however, zz does enforce api contracts which can be arbitrary expressions within the QF_UFVB theory. for example check out the err::checked() theory which enforces that a function call must be followed by err::check. similarly, i expect a community will come up with other standard contracts such as must_not_copy() for secret values that may not be copied.

by lwb 7y ago

augusto-moura 7y ago

In the README there's a example of proving a simple state machine open > read > close [1] Just read the docs™ [1] https://github.com/aep/zz#theory https://github.com/aep/zz#theory

lwb 7y ago
Ah ok, not sure how I missed that. That still seems to be within the realm of a type system, no? Or would you consider type systems a subset of mathematically provable systems?
- ludamad 7y ago
  Dependent type systems certainly are!
- augusto-moura 7y ago
  Well Type Theory is actually one of the definitions of mathematics and computation[1]. Wikipedia gives a basic definition of it [2][3] [1] https://en.wikipedia.org/wiki/Typed_lambda_calculus https://en.wikipedia.org/wiki/Typed_lambda_calculus [2] https://en.wikipedia.org/wiki/Type_theory https://en.wikipedia.org/wiki/Type_theory [3] https://en.wikipedia.org/wiki/Foundations_of_mathematics https://en.wikipedia.org/wiki/Foundations_of_mathematics
MaxBarraclough 7y ago
So it has typestates. (I recommend anyone [0] and its HN thread [1] for detail.) I think that's a great language feature for helping to avoid bugs, especially the kind that often happen in C, but I don't imagine it's anywhere close to proving whole-program correctness, is it? For the curious, here's an official example in the SPARK language, that gives a proven-correct sort function. (A complete proof of correct program behaviour, not just absence of undefined behaviour). As you can see, proving correctness is a challenge that permeates every inch of the code. [2][3] Microsoft's Dafny language is similar. [4] [0] https://yoric.github.io/post/rust-typestate/ https://yoric.github.io/post/rust-typestate/ [1] https://news.ycombinator.com/item?id=21413174 https://news.ycombinator.com/item?id=21413174 [2] https://github.com/AdaCore/spark2014/blob/76e08d279c/docs/ug/gnatprove_by_example/examples/sort.ads https://github.com/AdaCore/spark2014/blob/76e08d279c/docs/ug... [3] https://github.com/AdaCore/spark2014/blob/76e08d279c/docs/ug/gnatprove_by_example/examples/sort.adb https://github.com/AdaCore/spark2014/blob/76e08d279c/docs/ug... [4] https://en.wikipedia.org/wiki/Dafny#Imperative_features https://en.wikipedia.org/wiki/Dafny#Imperative_features
- augusto-moura 7y ago
  I imagine that whole-program correctness can be represented, but is not enforced in the case of ZZ. Developers are not obligated to declare typesets for their own code or can rely on other libraries being fully typed
  - MaxBarraclough 7y ago
    > not enforced in the case of ZZ I don't think it's really even possible for a language to force the programmer to give a proper formal specification. We may want the formal spec to grant some leeway, i.e. not to specify the exact output/behaviour, but instead to express certain important constraints. For instance, we may not care which traffic-light turns green first, so long as the system preserves the important properties about safety and liveness. If we wish to support such flexibility, we can't stop the programmer from expressing all output states are valid. If we don't wish to support such flexibility, what we're really doing is comparing against a reference implementation.
    - zozbot234 7y ago
      > I don't think it's really even possible for a language to force the programmer to give a proper formal specification. The language, probably not. The standard library can certainly require detailed-enough formal preconditions to make its code defect-free, meaning that any remaining bugs can then be directly traced to the programmer's code.
      - MaxBarraclough 7y ago
        You mean that, for instance, a standard-library generic sort function, might require that your comparator function behave correctly when the arguments are reversed? That's an interesting idea. Like Java interfaces, but with formal contracts. I doubt that putting these contracts into the standard-library would give you good proof-coverage though.
  - a3p 7y ago
    that is correct. however, zz does enforce api contracts which can be arbitrary expressions within the QF_UFVB theory. for example check out the err::checked() theory which enforces that a function call must be followed by err::check. similarly, i expect a community will come up with other standard contracts such as must_not_copy() for secret values that may not be copied.