Sabbatical Project Proposal

The purpose of the project

To develop software and a web site that enable computer people world wide to experiment with and use the MATHS language in developing software. The software will enable the creation of linked, mathematical, and searchable documentation in HTML, XML, and ASCII.

In my last sabbatical(Spring 1999)I published half-a-dozen samples of MATHS web pages. In the last seven years I have added more. [ samples/ ] About 40% of the pages were developed by students doing independent studies or course work. Now, I have a suite of tools that enable me to prepare web pages, bibliographies, mathematics (including proofs), and the formal documentation of software. Unlike other formal methods it does not use complex symbols but syntax inspired by programing languages. It creates linked and searchable documents for a topic or project. The same tool is used in all my classes to prepare handouts, visual aids, study guides, and Weblogs. Everyday hundreds of searches are carried out of various parts of the web site. In a recent interview about my FAR it was suggested that I should share my technology with more people.

It is not possible for people to use the tools to create their own pages without an account on our Computer Science network. It is difficult for students to use the tools because they are command-line driven. Before the start of the sabbatical I hope to fix this. The next step is to make the same functionality available to a worldwide clientele. My approach is inspired by the success of the open source movement(Linux, SourceForge, WikiPedia, WikiWikiWeb), some project development web sites (Google, Yahoo groups, and NSF FastLane for example), and the "Computer Reviews" web-site that let people edit shared documents via the web. I aim to create some similar functions for doing mathematical documentation. The system will enable web users to use plain ASCII text to create HTML pages, XML data, and possibly TeX documents.

The methods to be employed

The technology is well tested -- scripting languages running on a server. The site will use simple HTML pages, PHP, and either JavaScript or Java Applets to allow the input and editing of documents. A simple data base will handle content management. This prepares for the harder task of checking documents for inconsistencies and missing assumptions.

I will be using proven best-practices: iterative test-first development.

Each step will be recorded in a project Weblog.

A Brief timetable of activities

1. Translate existing shell scripts and C programs into web-based languages. (5 weeks)
2. Upload the existing bibliography (3,000 items) as a stress test.(1 week)
3. Instal or create a Content Management system to enable others to use the tools to collaborate on documents and the source code for the web site (2 weeks).
4. Upload samples and the formal definition of the MATHS language into the system(1 week).
5. Publicize the system and start monitoring the usage (1 week).

The proposed outcomes of the project

Papers in ACM SIGCSE Bulletin and articles in the IEEE Computer Magazine

The contribution of the project

This project will let me continue my 35-year study of software development methods & technology. The department will benefit from having a system for simple collaborative formal documentation for students and faculty. It will allow the department to take part in the Formal Methods Grand Challenge Project [Jim Woodcock, First steps in the verified software grand challenge, IEEE Computer Magazine V39n10(Oct 2006)pp57-64]. I hope to show, in the long term, how software development may become more reliable, given a simple & easy-to-use tool for logic & mathematics.

. . . . . . . . . ( end of section Sabbatical Project Proposal) <<Contents | End>>