Coq. Just because I‘ve seen it used successfully with code extraction in large scale projects.
Followers: Does any of you have an opinion on Coq vs Isabelle? (Especially in the context of formal hw verification, cc @rrika9, @alastair_d_reid)
-
-
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Of course, in terms of use as a programming language instead of as a proof assistant, F* beats them in terms of usability and proof flexibility. You might need to write your own HDL extraction for any of them, anyways.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Setting up Isabelle overflew my harddrive when I wanted to try it out so I skipped it ^^; I also seemed like my Coq skills weren't directly transferable.
-
We just started an internal Isabelle course in Arm Research. Will let you know when it is done. (I’m told that Coq dep types can get in the way but really useful for tricky stuff - but no direct experience).
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.