5 ms·

Can you expand on that a bit? If the program "is" the specification, in what manner could the program ever deviate from the specification in a way a prover coul

Can you expand on that a bit? If the program "is" the specification, in what manner could the program ever deviate from the specification in a way a prover could pick up? Or are you talking about adding additional constraints to a program in the same grammar as the code, such that a prover can demonstrate the program doesn't meet the constraint? (this still seems beneficial, but feels like encoding the spec together with the program - which isn't the same thing to my mind)

hansvm 5y ago
There's a linguistic sleight of hand going on here which I believe is the source of confusion. When you write a "specification" you're not just declaring properties that need to be proven; those properties refer to a model of your program which you also write as part of the spec (e.g., you don't just prove that when transferring money the total balance is constant; you require a model of what money is and how a transfer behaves). With that idea as the backdrop, TFA describes a system where you define a model, define properties that need to hold, prove those properties hold, and _also_ write a program that attempts to be a faithful representation of the model. Systems like coq [0] allow you to directly convert your model (which is proven to have the properties you desire) into something executable which also has those properties, ideally eliminating some toil and a potential source of errors. Does that help? [0] https://coq.inria.fr/refman/addendum/extraction.html https://coq.inria.fr/refman/addendum/extraction.html
- MaxBarraclough 5y ago
  > Systems like coq [0] allow you to directly convert your model (which is proven to have the properties you desire) into something executable which also has those properties, ideally eliminating some toil and a potential source of errors. How well does that work? A formal spec of stable-sort looks nothing like an efficient stable-sort implementation, and a formal spec for malloc and free looks nothing like an efficient implementation of the heap. Does Coq really auto-generate the whole solution, or is it 'guided' by the programmer toward an efficient algorithm?
  - jerome-jh 5y ago
    The extracted program is expected to be equivalent to the model in Coq. Target languages are all "safe" languages: OCaml, Haskell, Scheme, Elm. Algorithmically speaking, the extracted program is as optimized as it model.
    - MaxBarraclough 5y ago
      > Algorithmically speaking, the extracted program is as optimized as it model. Sounds like the Coq approach just shifts things around a little. Which is fine, but it seems less drastically different than I thought. I was taught formal methods in B-Method and Event-B. [0] (As an aside, I rather like Event-B, and it strikes me as a pity that more students aren't taught it.) They're imperative-oriented rather than functional-oriented but that's not the interesting difference here. In the lectures it was strongly emphasised that the initial mathematical modelling need only be correct, and that it made no sense to reason about its performance, as it was not intended to look anything like the eventual implementation. Put another way, the initial model is to specify the what, and should not concern itself with questions of how. Once the initial model is complete, you then refine the model iteratively until you have imperative code that can be rewritten (ideally automatically [1]) in a 'real' programming language like C or Ada. A modelling of malloc is likely to boil down to a mathematical such that expression expressing that it must always return a value with the necessary properties, and handle state appropriately, while saying nothing on how it does this. Part of the refinement process is to eliminate such that expressions, replacing them with imperative steps that provably satisfy the expression. (More precisely, it must provably satisfy all postconditions and invariants.) In short then, in Event-B you must refine your model down to something that maps naturally to imperative code. It sounds like Coq takes a somewhat different approach: you aren't required to refine your model all the way down. Instead, Coq will accept a partially refined, or even entirely unrefined model, and it will have a go at synthesising an implementation. With Coq then, good refinement may presumably be necessary for good performance, but you have the option of declining to fully refine your model. (Of course, the same approach could be taken with Event-B. I don't think it's generally done that way though, but I could be mistaken.) > Target languages are all "safe" languages I imagine that's just because functional languages tend to be safe, right? The existence of unsafe features in those languages wouldn't be a hindrance to Coq. [0] https://en.wikipedia.org/wiki/B-Method https://en.wikipedia.org/wiki/B-Method [1] https://wiki.event-b.org/index.php/Code_Generation_Activity https://wiki.event-b.org/index.php/Code_Generation_Activity

hansvm 5y ago

There's a linguistic sleight of hand going on here which I believe is the source of confusion. When you write a "specification" you're not just declaring properties that need to be proven; those properties refer to a model of your program which you also write as part of the spec (e.g., you don't just prove that when transferring money the total balance is constant; you require a model of what money is and how a transfer behaves). With that idea as the backdrop, TFA describes a system where you define a model, define properties that need to hold, prove those properties hold, and _also_ write a program that attempts to be a faithful representation of the model. Systems like coq [0] allow you to directly convert your model (which is proven to have the properties you desire) into something executable which also has those properties, ideally eliminating some toil and a potential source of errors. Does that help? [0] https://coq.inria.fr/refman/addendum/extraction.html https://coq.inria.fr/refman/addendum/extraction.html

MaxBarraclough 5y ago
> Systems like coq [0] allow you to directly convert your model (which is proven to have the properties you desire) into something executable which also has those properties, ideally eliminating some toil and a potential source of errors. How well does that work? A formal spec of stable-sort looks nothing like an efficient stable-sort implementation, and a formal spec for malloc and free looks nothing like an efficient implementation of the heap. Does Coq really auto-generate the whole solution, or is it 'guided' by the programmer toward an efficient algorithm?
- jerome-jh 5y ago
  The extracted program is expected to be equivalent to the model in Coq. Target languages are all "safe" languages: OCaml, Haskell, Scheme, Elm. Algorithmically speaking, the extracted program is as optimized as it model.
  - MaxBarraclough 5y ago
    > Algorithmically speaking, the extracted program is as optimized as it model. Sounds like the Coq approach just shifts things around a little. Which is fine, but it seems less drastically different than I thought. I was taught formal methods in B-Method and Event-B. [0] (As an aside, I rather like Event-B, and it strikes me as a pity that more students aren't taught it.) They're imperative-oriented rather than functional-oriented but that's not the interesting difference here. In the lectures it was strongly emphasised that the initial mathematical modelling need only be correct, and that it made no sense to reason about its performance, as it was not intended to look anything like the eventual implementation. Put another way, the initial model is to specify the what, and should not concern itself with questions of how. Once the initial model is complete, you then refine the model iteratively until you have imperative code that can be rewritten (ideally automatically [1]) in a 'real' programming language like C or Ada. A modelling of malloc is likely to boil down to a mathematical such that expression expressing that it must always return a value with the necessary properties, and handle state appropriately, while saying nothing on how it does this. Part of the refinement process is to eliminate such that expressions, replacing them with imperative steps that provably satisfy the expression. (More precisely, it must provably satisfy all postconditions and invariants.) In short then, in Event-B you must refine your model down to something that maps naturally to imperative code. It sounds like Coq takes a somewhat different approach: you aren't required to refine your model all the way down. Instead, Coq will accept a partially refined, or even entirely unrefined model, and it will have a go at synthesising an implementation. With Coq then, good refinement may presumably be necessary for good performance, but you have the option of declining to fully refine your model. (Of course, the same approach could be taken with Event-B. I don't think it's generally done that way though, but I could be mistaken.) > Target languages are all "safe" languages I imagine that's just because functional languages tend to be safe, right? The existence of unsafe features in those languages wouldn't be a hindrance to Coq. [0] https://en.wikipedia.org/wiki/B-Method https://en.wikipedia.org/wiki/B-Method [1] https://wiki.event-b.org/index.php/Code_Generation_Activity https://wiki.event-b.org/index.php/Code_Generation_Activity