![]() ![]() The thing is that the sort of proofs that show up here are fine and all, but they aren't going to teach you to fish for yourself. Because the Z3 tutorial was designed for automation, the more automated tactics in MicroOmega and Ring are super useful. It's interesting the things that show up. For the most part I think it isn't that hard and rather educational. “What could even be the problem?”Īnyway, a fun exercise for me was to take the examples from my tutorial and try to translate them into Coq. I say this to Coq users and they look at me like I’m nuts. For example, defining an inductive predicate as a datatype is still a bizarre notion to me, but it is Coq 101. But Coq users, this is just the water they swim in. I still think many aspects of it are totally bizarre. ![]() Coq is a tool that requires significantly more background to even comprehend what the hell it is.Z3 can actually be used to declaratively state problems and pushbutton calculate solutions to them with very little user help, which gives it a lot more "Wow" factor.I could use Z3’s python bindings giving an air of familiarity, whereas everything was incredibly foreign in Coq.There are a number of factors to lead to this: He knew it was going to be like this from the outset and had a fun little analogy of me downhill skiing while he was about to go on an uphill mountaineering slog. ![]() It was a fantastic tutorial (maybe the best I've seen?), but it was tough love. I got to be kind of the "fun dad" with the Z3 tutorial, while at times it felt a bit like Cody's Coq tutorial was trying to feed the kids their vegetables. I had a fun time giving a Z3 tutorial at Formal Methods for the Informal Engineer (FMIE) (videos coming soon hopefully!). ![]()
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |