3 ms·

The extracted program is expected to be equivalent to the model in Coq. Target languages are all "safe" languages: OCaml, Haskell, Scheme, Elm. Algorithmically

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.

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.