Current Status: Trying to learn a new thing.
I think they called it Coq because it's hard.. (Sorry 
)pic.twitter.com/3WQHw8ytIX
-
What sort of proofs are you looking towards doing? I had a lot of fun learning it with group theory proofs.
The ambitious goal is to prove properties of digital hardware in coq. Part of that project will be a coq back-end for Yosys. Thankfully @rrika9 said she'd help, otherwise I'd be lost.
-
-
what kind of "property" coq will be able to prove on a digital hardware that a SMT solver like Z3 can't ?
-
Well, coq can't prove anything. It can just check if the proofs you give it are correct. :) There is a lot of stuff involving algebra that humans can solve pretty easily and bit-vector SMT solvers can't. For example, try this with N, M > 16: http://svn.clifford.at/handicraft/2017/vlcoqex/mulequiv.sv …pic.twitter.com/k9BKsKCikV
- Show replies
New conversation -
-
-
I've just run into a simple property that symbiyosys got stuck on for half an hour before I gave up (thanks, multiplication!), so now I'm looking forward to progress on this.
-
^^;;;;;;.
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.