Huỳnh Trần Khanh (Jan 29 2023 at 15:03): Huỳnh Trần Khanh (Jan 29 2023 at 15:03):It's been a few days. I'm still working hard on that exchange argument! I feel like I think so slowly, I can't type the commands quickly enough. And for some lemmas I kept trying many different approaches to prove. So many false approaches! Eventually I found one that worked, but the speed is too slow I'm afraid I can't compete with other more experienced folks. I don't have to look up the Coq documentation much, I already memorize the most important commands and can search for existing lemmas in stdpp quickly enough, so familiarity with Coq is not the bottleneck here. I feel my intuition is weak. I am particularly slowed down when I have to delete the code for a lemma and prove it again because my approach is entirely wrong, or I suddenly find out that I can't do induction because reasons. The statement not being strong enough is a common one, but sometimes my approach is just entirely wrong and I'm stuck trying to force induction into the problem. Do you feel the same way sometimes, and how do you improve your intuition?
Coq's performance really exposes my weakness. In the past, I used Lean, and as Lean is very slow (you need to push your code to CI often as your machine can't process the code) I felt like Lean's speed was the bottleneck. Now I'm the slow one here.
Karl Palmskog (Jan 29 2023 at 15:16):are you sure what you are proving is true? According to our survey, quite a few people are using tools like QuickChick to check properties for concrete values before they do the proof.
Karl Palmskog (Jan 29 2023 at 15:19):using Coq is sometimes not all that different from any kind of math problem solving, so the usual heuristics may help: https://en.wikipedia.org/wiki/How_to_Solve_It
Paolo Giarrusso (Jan 29 2023 at 17:37):A kind of common advice: try to sketch proofs on paper. Think of it as writing pseudocode: it lets you iterate faster, and without computer feedback it forces you to focus on the higher-level ideas.
Paolo Giarrusso (Jan 29 2023 at 17:38):I think it can be tricky without mathematical training, but you're training with Coq, so with practice you should be able to recognize arguments that you can formalize vs arguments that need details vs fallacies, and/or refine that.
Paolo Giarrusso (Jan 29 2023 at 17:42):Having false approaches is normal, and that's one reason to sketch proofs.
Paolo Giarrusso (Jan 29 2023 at 17:43):I should say: I've written proof sketches that I thought didn't work (because they involved non-well-founded recursion) and turned out to actually work later. But I don't think that's common.
Paolo Giarrusso (Jan 29 2023 at 17:47):Last thing: there are proofs that are quicker to do in Coq than sketch on paper; for a trivial instance, large boring cases analyses or calculations: maybe you can do a couple cases by hand. I don't have a general strategy to explain, other than "mix and match", especially because what's faster depends on your strength and varies with your experience. You'll have to practice to recognize which ones.
Huỳnh Trần Khanh (Jan 30 2023 at 06:36):How fast do you usually come up with lemmas, definitions, algorithms and prove them? In a web application for example there are many features, and we need to prove that all features work correctly. And also because business requirements change frequently we have to code and prove the features quickly enough to deploy them to customers. Web applications are also insanely complicated because they have to be distributed across many servers in many geographical regions.
Paolo Giarrusso (Jan 30 2023 at 10:53):That sounds like a different topic: often many other problems would come up before (sequential) algorithmic verification.
Last updated: Jun 05 2023 at 10:01 UTC