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

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.