Hi Ramana, I'm not quite sure how to interpret your question. Are you suggesting that HOL4's user interface, with it's existing provision for mixing declarative and imperative styles, is perfectly good already, or are you suggesting that it's difficult to get any better (regardless of whether it's perfectly good)? I disagree with both, but it's difficult for me to defend my position without an actual implementation of my system to back me up.
Mark. on 12/7/12 8:11 AM, Ramana Kumar <[email protected]> wrote: > On Wed, Jul 11, 2012 at 8:38 PM, "Mark" <[email protected]> wrote: > >> I intend to cater for both the declarative style (i.e. stating the result >> of >> the step) and the imperative style (i.e. stating what operation to apply >> next), and a mixture of both. I think that this is a huge subject that > has >> not been properly explored yet by existing systems. > > I would say one can write proof scripts in a mixture of imperative and > declarative styles already in HOL4, in particular using things like "by", > "TRY", and the various matching, renaming, and abbreviating tactics for the > declarative parts. It's a matter of self-discipline how much you want to > explicitly state formulae you're proving or manipulating. Is there > something more to declarative proofs that I'm missing? ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
