4 ms·

> 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 tho

> 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
  - jerome-jh 5y ago
    Coq is at its core a typed functional language. Algorithms to be studied are expressed in this language and they live in a type "hierarchy" called Set. The same language is used to construct proofs about algorithms. They live in a different type "hierarchy" called Prop and use a different syntax at places for convenience and to make proofs look like usual mathematics. The extraction of the algorithms expressed in Coq to another typed functional language such as OCaml is pretty straightforward and natural. But since Coq is purely functional, modelling a memory allocator is of little practical use. The malloc model would basically return a pointer to allocated memory and a full copy of the memory heap. It is probably still worthwhile to prove properties of the algorithm, but the extracted program in this case cannot be used as is.
hansvm 5y ago
Efficiency depends on a sufficiently smart compiler. That's not as bad as it sounds because the conceptual mismatch between formal specs and machine code that you're alluding to isn't as bad in Coq as in, say, typical TLA+. You do have heaps and whatnot available.
- pron 5y ago
  That is very inaccurate. TLA+ is normally used for things that are much bigger than Coq could feasibly be used for at all. They're aimed for programs of completely different orders of magnitude. TLA+ is commonly used by engineers to specify and check systems or components with tens of thousands or hundreds of thousands of lines over, say, a couple of weeks. Coq and other things that are more aimed at end-to-end verification, all the way to code, have only ever been used on programs or components less than 10KLOC, and even then required teams of world-experts working for years.
  - hansvm 5y ago
    > That is very inaccurate. Nah, we just didn't talk about the downsides you're mentioning. The fact that there are downsides doesn't make everything else false. > 10KLOC ~100KSLOC (e.g., CompCert) > and even then required teams of world-experts working for years Definitely. A future might exist where computers are fast enough and where we've uncovered better algorithms in that space so that something else could take the place of Coq and lessen that workload to something manageable for a typical project, but it's pretty hard to use right now.
    - kaba0 5y ago
      As far as I know formal verification doesn’t necessarily give way for much parallelism, and the halting problem will not become obsolete, and the latter is a lower bound on many interesting properties. So unless there is a radically new way to serial computations, that is orders of magnitude faster, I doubt much would change. CPUs are already quite at the limit with super-scalar architectures.

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
- jerome-jh 5y ago
  Coq is at its core a typed functional language. Algorithms to be studied are expressed in this language and they live in a type "hierarchy" called Set. The same language is used to construct proofs about algorithms. They live in a different type "hierarchy" called Prop and use a different syntax at places for convenience and to make proofs look like usual mathematics. The extraction of the algorithms expressed in Coq to another typed functional language such as OCaml is pretty straightforward and natural. But since Coq is purely functional, modelling a memory allocator is of little practical use. The malloc model would basically return a pointer to allocated memory and a full copy of the memory heap. It is probably still worthwhile to prove properties of the algorithm, but the extracted program in this case cannot be used as is.

hansvm 5y ago

Efficiency depends on a sufficiently smart compiler. That's not as bad as it sounds because the conceptual mismatch between formal specs and machine code that you're alluding to isn't as bad in Coq as in, say, typical TLA+. You do have heaps and whatnot available.

pron 5y ago
That is very inaccurate. TLA+ is normally used for things that are much bigger than Coq could feasibly be used for at all. They're aimed for programs of completely different orders of magnitude. TLA+ is commonly used by engineers to specify and check systems or components with tens of thousands or hundreds of thousands of lines over, say, a couple of weeks. Coq and other things that are more aimed at end-to-end verification, all the way to code, have only ever been used on programs or components less than 10KLOC, and even then required teams of world-experts working for years.
- hansvm 5y ago
  > That is very inaccurate. Nah, we just didn't talk about the downsides you're mentioning. The fact that there are downsides doesn't make everything else false. > 10KLOC ~100KSLOC (e.g., CompCert) > and even then required teams of world-experts working for years Definitely. A future might exist where computers are fast enough and where we've uncovered better algorithms in that space so that something else could take the place of Coq and lessen that workload to something manageable for a typical project, but it's pretty hard to use right now.
  - kaba0 5y ago
    As far as I know formal verification doesn’t necessarily give way for much parallelism, and the halting problem will not become obsolete, and the latter is a lower bound on many interesting properties. So unless there is a radically new way to serial computations, that is orders of magnitude faster, I doubt much would change. CPUs are already quite at the limit with super-scalar architectures.