On Thu, Jul 12, 2012 at 11:37 AM, Freek Wiedijk <[email protected]> wrote:
> Hi Mark,
>
> >It's just that no-one's done it yet!
>
> 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.
>
One way to ameliorate this problem is to compose proofs lazily.
By that, I mean when you get to a step that's obvious to you, just cheat
(most proof assistants have some option to make a "tagged" theorem without
proof).
Later, after a long exploratory theory development, having settled on the
right structures, you can go back and fill in the cheats with real proofs,
or pass that task off to better automation (if someone implemented it), or
to someone else.
A lot of them will probably disappear before getting proved (which means
work is avoided), as you figure out the high-level structure of the theory.
The proof assistant doesn't really force you to focus on all the details;
in some ways that is just a habit, perhaps reinforced by the interface.
>
> 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
>
------------------------------------------------------------------------------
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
