On Thu, Jul 12, 2012 at 3:37 AM, Freek Wiedijk <[email protected]> wrote:
> Hi Mark,
>
> >It's just that no-one's done it yet!
>
This from Mark was a reply to my comment that making a proof assistant
really easy to use will be "a huge challenge". I was speaking from a
software engineering and usability point of view. In particular I'm
thinking of usability by people who are not steeped in the culture of
formal logic, people who have some exposure to math, but not to
higher-order logic or even perhaps formal logic.
In reality this "ease of use" question is many-faceted. It depends on what
we mean by easy and who we think the users may be. I have a particular
personal interest in having a proof assistant that is easy enough to use
that "way more people" will decide it is their personal preferred way to
get symbolic mathematics done without having to be told by a professor, and
without it being an overriding requirement of a project where an error in
reasoning may cost millions of dollars (or pounds, or Euro's, etc.).
Freek, I do like your two points as being key, especially your point 2.
Point 1 may be especially important for users who are trained
mathematicians, and certainly worth stating.
Point 2 I think is more a question of software design. HOL Light for
example has bazillions of tactics and rules of inference and theorems, all
with names to be remembered. By my definition of easy, this is much too
hard. The tool needs to guide the user toward relevant options (and not to
_all_ options), ideally ones that seem particularly likely to be useful as
well.
Even issues like being able to read a completed proof, or follow the steps
or get explanations for them are things I consider important for adoption
by many people. But in the end here I am agreeing with you all, and trying
to clarify, not dispute.
Regards,
Cris
>
> There are just two things that make proof assistants
> difficult to use:
>
> 1. There is not sufficient automation of trivial stuff.
>
> I.e., you generally need to break down your reasoning into
> smaller steps than how you would experience things when
> you wouldn't be dealing with a proof assistant. Maybe you
> _would_ experience those steps very fleetingly, but you
> wouldn't focus at them in the way a proof assistant
> forces you to. It's like doing math veeeerrrrryyyy
> sllloooowwlllllyyy.
>
> If some step in a proof is obvious to you, you want to be
> able to just say "well, that's obvious" and nothing more.
> That's unfortunately not how it seems to work right now.
> Even if there's automation in a system that can solve
> such a problem, you need to be aware _what_ automation
> to invoke.
>
> 2. You need to be able to find things in a library, or
> establish that the thing you think you need is not
> there yet.
>
> And you need to be able to keep your library
> well-organised and in sync with the versions of your
> systems. Not easy.
>
> Random example: suppose you want to use Schwarz's
> inequality in a proof. So _here's_ your formalisation
> that you're working on, and _there's_ the library of your
> system. Now what? You will need to give search commands,
> or switch windows to look at lists of things you might
> need, or try to remember what the lemma was called and
> what was its exact shape... it's all irritating overhead.
>
> And when you prove something you will need to decide
> on a name for your new lemma. That's something that's
> particularly difficult.
>
> There are no other reasons proof assistants are difficult.
> So will these be the two things you'll be addressing?
>
> Of course these two things are related. And Sledgehammer
> clearly is trying to address these problems. But yes,
> it's not fully "done yet".
>
> Freek
>
------------------------------------------------------------------------------
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
