4 ms·

Running tokei [0] on their repo [1] gives me that it's around 300 lines of C, and around 8000 lines of Coq. A lot of that C is actually test code, so in reality

Running tokei [0] on their repo [1] gives me that it's around 300 lines of C, and around 8000 lines of Coq. A lot of that C is actually test code, so in reality it's about 8000 lines of Coq to prove around 150 lines of C correct. They also don't prove the correctness of mmap (which is how they actually get memory to alloc out), but entirely depend on it. It seems incredibly expensive to write 8000 lines of very dense and difficult proof code in order to verify that you remembered to check "if p == NULL". It probably would turn null into a trillion dollar mistake if all devs had to write coq proofs for each nullcheck. 0: https://github.com/XAMPPRocky/tokei https://github.com/XAMPPRocky/tokei 1: https://github.com/PrincetonUniversity/DeepSpecDB/tree/05bd75f8c3a22267c27d5ab94e5f03b610797cf7/memmgr https://github.com/PrincetonUniversity/DeepSpecDB/tree/05bd7...

stefan_ 7y ago
They prove a lot more, e.g. that if you have an oracle that can guess the total amount of memory needed beforehand, during runtime the malloc call will never fail if you stay under the amount. But of course it's rabbit holes all the way. Whatever application uses this allocator also needs to be verified, where then you need to prove that there is never a sequence of malloc/free calls that will exceed this limit.
zozbot234 7y ago
> A lot of that C is actually test code, so in reality it's about 8000 lines of Coq to prove around 150 lines of C correct. I wonder how much of that proving burden would be subsumed by rewriting those 150 lines of C into idiomatic Rust. Though the real problem with Coq/Isabelle/Lean/etc. proofs is not the LOC's but the brittleness of their "proof script"-based approach. Sensible ITP systems are based on a declarative approach where the "strategy" used in any given proof step is secondary, while the semantics of the step itself is stated very clearly and explicitly. This makes the proof script robust to changes in other portion of the code, so that even 8k lines of proof becomes more easily manageable.
- p0llard 7y ago
  This is a common criticism of tactic based proofs, but the style that's being adopted more and more involves heavy use of proof automation which allows fairly major changes to be made without breaking the proof script.
  - zozbot234 7y ago
    From this POV, proof automation just enables bigger proof steps. Of course, sometimes the inputs to the "automation" are enough to disambiguate the logical step on their own (e.g. whenever a lemma is proved in a single "auto" step, though this is far from a novel approach!) but declarative proofs are nonetheless a more consistent solution to this issue.

stefan_ 7y ago

They prove a lot more, e.g. that if you have an oracle that can guess the total amount of memory needed beforehand, during runtime the malloc call will never fail if you stay under the amount. But of course it's rabbit holes all the way. Whatever application uses this allocator also needs to be verified, where then you need to prove that there is never a sequence of malloc/free calls that will exceed this limit.

zozbot234 7y ago

> A lot of that C is actually test code, so in reality it's about 8000 lines of Coq to prove around 150 lines of C correct. I wonder how much of that proving burden would be subsumed by rewriting those 150 lines of C into idiomatic Rust. Though the real problem with Coq/Isabelle/Lean/etc. proofs is not the LOC's but the brittleness of their "proof script"-based approach. Sensible ITP systems are based on a declarative approach where the "strategy" used in any given proof step is secondary, while the semantics of the step itself is stated very clearly and explicitly. This makes the proof script robust to changes in other portion of the code, so that even 8k lines of proof becomes more easily manageable.

p0llard 7y ago
This is a common criticism of tactic based proofs, but the style that's being adopted more and more involves heavy use of proof automation which allows fairly major changes to be made without breaking the proof script.
- zozbot234 7y ago
  From this POV, proof automation just enables bigger proof steps. Of course, sometimes the inputs to the "automation" are enough to disambiguate the logical step on their own (e.g. whenever a lemma is proved in a single "auto" step, though this is far from a novel approach!) but declarative proofs are nonetheless a more consistent solution to this issue.