Le 02.04.13 23:10, Bill Richter a écrit : > Thanks, Vince! Can you remind me about your module & tactics that improve > readability, with fewer type annotations? To remove type annotations, see the Q-like module at http://users.encs.concordia.ca/~vincent/Software.html (note that this is present by default in HOL4). For the tactics, see my messages on this mailing list. But I'm preparing something more general and better that I'll release within 2 months, maybe it will be satisfying to you...
> I generally prefer the usual tactic style rather than the > declarative style. > > I don't tend to think these words are too helpful. The important words are > readable and powerful (rather than declarative and procedural), and we want > both. My code hol_light/Examples/inverse_bug_puzzle_tac.ml uses tactics, and > I think the proofs are quite readable if you first turn it into an > interactive proof, evaluate it, and look at the output. It's very similar > to hol_light/Examples/inverse_bug_puzzle_miz3.ml, which is however a lot more > readable if you just read the code. So what I want is to make > inverse_bug_puzzle_tac.ml more readable without interactive/evaluation. > Isn't that the sort of thing you're doing? Haha, no: my proofs are unreadable without the interactive/evaluation! And this is where I say that I disagree with what is usually presented as the declarative style (I think miz3 is more than just a usual declarative style though): I don't believe that scripts should look like mathematical proofs. I believe that there should be powerful tactics which would correspond to "big steps" in a proof. But I want the outcome of these big steps to be obtained by interaction with the machine, instead of being given explicitly by the human. I will hopefully write a paper on this and explain my views and the underlying reasons in more details. Cheers, -- Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware Verification Group http://users.encs.concordia.ca/~vincent/ ------------------------------------------------------------------------------ Minimize network downtime and maximize team effectiveness. Reduce network management and security costs.Learn how to hire the most talented Cisco Certified professionals. Visit the Employer Resources Portal http://www.cisco.com/web/learning/employer_resources/index.html _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
