3 ms·

Verified Vector Clocks: An Experience Report, Part 2

29 points by cmeiklejohn 13y ago

axman6 13y ago
As someone quite familliar with Haskell, I found the code here almost unreadable. I guess Coq is a log way away from Haskell.
- cmeiklejohn 13y ago
  It's definitely not implemented in the most-efficient manner. If you look at the commit history for the repo, a ton of the functions which were normally partially applied had to either be inlined or broken out else it broke the Core Erlang extraction; mainly because it produced code which wouldn't be compiled by the Erlang compiler. Also, I tried writing it to be as close to the original Erlang as possible to make the post a bit more compelling and understandable for Erlang developers familiar with Riak. However, that being said it should be pretty readable to an OCaml developer: Here's the link to the first post, which discusses problems with the Core Erlang extraction and the original version of the code: http://christophermeiklejohn.com/coq/erlang/2013/11/04/verified-vector-clocks-an-experience-report-part-1.html http://christophermeiklejohn.com/coq/erlang/2013/11/04/verif...
biscarch 13y ago
Awesome! I highly enjoyed the related talk at RICON West and it's nice to see the code and process laid out.
- cmeiklejohn 13y ago
  Thanks!
colanderman 13y ago
Why define Notation for pairs and then not use it? Instead of using match/with/true/false, you can use if/then/else. Verlang looks great. Will have to try it out. Strange that Verlang generates uncurried functions. I know that's not the default in Erlang, but as you found out, it breaks extraction.
- cmeiklejohn 13y ago
  Noted. I didn't define that notation, I just simply pasted in what's in the Coq standard library so it would be clear how the triple constructor worked. Agreed, could use if. I mainly used match with the true/false branches to make it as close to the original Erlang as possible, for readers unfamiliar with the Coq syntax.

3 ms·

Verified Vector Clocks: An Experience Report, Part 2

29 points by cmeiklejohn 13y ago

axman6 13y ago
As someone quite familliar with Haskell, I found the code here almost unreadable. I guess Coq is a log way away from Haskell.
- cmeiklejohn 13y ago
  It's definitely not implemented in the most-efficient manner. If you look at the commit history for the repo, a ton of the functions which were normally partially applied had to either be inlined or broken out else it broke the Core Erlang extraction; mainly because it produced code which wouldn't be compiled by the Erlang compiler. Also, I tried writing it to be as close to the original Erlang as possible to make the post a bit more compelling and understandable for Erlang developers familiar with Riak. However, that being said it should be pretty readable to an OCaml developer: Here's the link to the first post, which discusses problems with the Core Erlang extraction and the original version of the code: http://christophermeiklejohn.com/coq/erlang/2013/11/04/verified-vector-clocks-an-experience-report-part-1.html http://christophermeiklejohn.com/coq/erlang/2013/11/04/verif...
biscarch 13y ago
Awesome! I highly enjoyed the related talk at RICON West and it's nice to see the code and process laid out.
- cmeiklejohn 13y ago
  Thanks!
colanderman 13y ago
Why define Notation for pairs and then not use it? Instead of using match/with/true/false, you can use if/then/else. Verlang looks great. Will have to try it out. Strange that Verlang generates uncurried functions. I know that's not the default in Erlang, but as you found out, it breaks extraction.
- cmeiklejohn 13y ago
  Noted. I didn't define that notation, I just simply pasted in what's in the Coq standard library so it would be clear how the triple constructor worked. Agreed, could use if. I mainly used match with the true/false branches to make it as close to the original Erlang as possible, for readers unfamiliar with the Coq syntax.