Functionality

1. The user interface must be able to run on most common personal computers.
2. The proof assistant being used should be applicable to a wide range of logics, and easily extensible to new logics.
3. The system should be built entirely of free software,The Free Software Foundation: http://www.fsf.org/. as much as possible.
4. The system should be simple to adapt to future needs.

The simplest of user interfaces will be of limited value if the system does not meet a reasonable standard of functional requirements.

Our first functional requirement is that the interface is available on a range of operating systems covering the majority of potential users. The target platforms are therefore defined as Microsoft Windows, Macintosh operating systems (OS9 and earlier, as well as OSX) and X11/unix (Linux, FreeBSD etc). This covers both technical user communities (frequently making use of unix variants), and less technical user communities that tend to favour single user operating systems. §4.1 discusses the choice of programming languages and library toolkits to achieve this result.

The second requirement is that the interface be available for use in a wide range of logics, thereby avoiding the need for users to learn multiple programs in order to prove in different logical frameworks. Solutions to this are given in §4.6.

The next requirement (free software licencing) attempts to allow as large a community to benefit from the system as possible. This allows the system to evolve to the needs of users easily and quickly. Candidate licencesA large list of licenses approved by the Open Source Initiative is available at their website:
http://www.opensource.org/licenses/index.php may include the GNU General Public License, the BSD License and the Apache Software License. This is addressed in §4.

The final functional requirement ensures that the system is useful for as long as possible.

A well defined and documented organisation of the code comprising the system is needed to ensure that the previous point can be exploited to maximum benefit. This is addressed in §4.