----------------------------------------------------------------------------
Thanks for agreeing to participate in the FM Outreach meeting at SRI
on June 9 and 10.  We will have a dinner on Mon June 9.  The meeting
will last until lunch time on Tue June 10, and the anyone remaining
can help draft a summary of the meeting.

The goal of the meeting is to develop strategies for the creative use
of formal modeling and analysis tools in education and industry.  In
concrete terms, we should draft a ten to twenty page document
outlining the challenges and outreach opportunities for formal
methods, in particular, and computational methods, in general.  Please
send me a title for a short (possibly informal) talk with a discussion
exploring some of the challenges and opportunities for formal methods.
I would also like a few sentences summarizing a position statement.

Here are some of the basic discussion points (but the meeting is by no
means limited to these):

1. Formal methods are at a crossroads: On the positive side, the
technology is well developed and there are a large number of interesting
applications.  However, on the negative side, it no longer viewed as
part of mainstream computing, and does not draw many graduate students.

2. The subject matter of formal methods is both exciting and increasingly
relevant.  With the dramatic increase in computing power over the last
decade, we are now in a position to lift computing to the semantic realm of
models and inference.  This shift enables a number of novel applications in
education and industry.  As examples, we can now model both digital and
analog hardware, mathematical theories, static and dynamic physical systems,
biological networks, complex software systems, and even human psychology and
social interactions.

3. Education at all levels can benefit from formal modeling and analysis,
and the deeper use of computational metaphors and algorithmic insights.
Currently, computing is taught in terms of low-level information processing
tasks whereas the real insights are obtained from the use of computational
models and computation.

4. The industrial uptake of formal methods can also be broadened.
Currently, a few industries are both producers and consumers of formal
tools.  For example, Intel and AMD use such tools for checking circuit
equivalence, generating test sequences, model checking finite-state
controllers, and proving theorems about floating-point arithmetic
algorithms.  Microsoft has a number of projects that employ software model
checking and automated reasoning to analyze sequential code for termination,
assertional correctness, and absence of races and deadlocks.  However, these
are still relatively modest efforts compared to the systematic use of formal
tools across the entire process.  We are not suggesting that the technology
is ready for such wider use, but that it is time to contemplate more
ambitious and non-traditional applications.

5. Both in education and industry, tools must actively support
collaboration.  Students learn from doing rather than being told,
and from interacting with their peer group at least as much as
their teachers.  Formal tools should be set up to promote cooperation
between different users so that they can share results and exchange
criticism.

6. Can we identify projects in different knowledge disciplines that
synergistically combine knowledge, deduction, and search to deliver
training, insight, and social collaboration in a form that is stimulating
and entertaining?  Mathematics itself can benefit from algorithmic ideas if
its results can be interpreted as providing algorithmic building blocks.

In summary, now is the time to think radical thoughts about new approaches
to educational and industrial applications of technologies for formal
modeling and problem solving skills needed for the twenty-first century.
----------------------------------------------------------------------------