Proposed new feature: Provers

[David A. Wheeler]

The "Provers" work wasn't just a few random packages with no purpose.
The point is to get a suite of tools to people who are trying to build
_highly_ reliable software/hardware (e.g., where ANY error is
likely to kill lots of people, etc.).  You end up needing a suite of tools,
and we've also been working hard to improve how they work together.
"Why" in particular really requires a passel of other tools to be useful.

Please look at the details; if that's not clear, please help me fix it!

http://fedoraproject.org/wiki/Features/Policy/Definitions
says:
>A feature is defined as a significant change or enhancement to the version of Fedora >currently under development that may or may not include new packages.

So a feature _can_ involve adding new packages.

>Features are usually considered to meet one or more of the following objectives:
>   1. highly user visible changes (beyond artwork or theme changes)

If you develop these kinds of programs, adding this suite of tools
(and thus this capability) is highly visible.

>   2. improvements or changes that require non-trivial cross-package integration

The "Why" suite depends on other tools, particularly Coq and Zenon.
But Why generated the wrong version of Zenon input; we had track that problem
down, and we worked with upstream to fix it.  In fact, the "Why" folks
created a new release for us, so that we could package one that worked
with Zenon.

The "Why" suite actually can call lots of provers, the more the better
(it tries different ones to see if any can succeed).  I hope to get more
added over time.  But having the infrastructure in place is the first step;
we can now add others and have them work together.

>   3. exciting new capabilities we can trumpet fedora having--some of this is good public relations. Some examples might include:
>          * new features from upstream that we are making available in the Fedora for the first time

I think this counts.

>   5. noteworthy enough to call out in the release notes 

I think this applies too.

>   5. Are you trying to promote this package as a Feature for publicity reasons?

Frankly, yes.

This is a lot like the "Haskell Support" of Fedora 10,  "TeXLive" of Fedora 9,
and "Electronic Lab" of Fedora 8.  Not _EVERY_ user of Fedora will
want these capabilities, but there _IS_ a user community which IS interested.
I'm also hoping to (over time) expand that community, but step 1 is make it
easy enough to get and use the tools (so that those who might be interested
can try them out).

--- David A. Wheeler