Re: [Ufmrg] [EXT] Re: A few questions about UFMRG goals

Hi Joshua,

One piece of feedback I get when I ask people why they don't use formal
methods is that there is no intermediate level training available.

There is documentation for some tools, and sometimes YouTube tutorials for
the basics, but unless you work with the tool authors, or people
experienced in modelling, there isn't somewhere to learn all the tips and
tricks necessary to prove complex things. So people get through a very
basic tutorial, and then go look at papers that include huge, complex
models, and have no idea how to get between those two places.

The goal of the training is to hopefully build up a set of recorded pieces
of training that help people use the tools as they are. By running multiple
trainings the hope is to provide a pathway, along with a place you can go
and ask questions of experts.

Certainly one of my hopes for this group is that we can provide actionable
feedback to tool authors so that they can improve their tools, but starting
with the things we can achieve without going outside the group seems like
the best way to get started.

Another thing I think we can do fairly immediately is provide guidance on
which tools might be most appropriate for which tasks, and thus help work
out what work needs to be done to prove the properties we want.

So overall I agree with Stephen's 1c, and mostly 2c. I think the training
(along with making the materials available) does make the tool more
useable, even though I agree a proper usability study would be even better.
I do think there are a number of easy usability improvements to be had in
many tools before we need to go for a usability study, so I don't think
we're completely unable to proceed on that front.

We are definitely looking for people who have a background in things like
user studies to help us make both the training and the group overall a
success, so if you have suggestions (or even suggestions of people we can
ask) they would be very gratefully received.

Regards,

Jonathan

On Thu, 7 Sept 2023, 23:04 Joshua D Guttman, <guttman@mitre.org> wrote:

> I was really impressed by the fast three minute
>
> response, just before the interim mtg a week ago.
>
>
>
> But I'm not sure that the reply really gets to the
>
> heart of the matter.
>
>
>
> You write:
>
>
>
> >    1(c) is fine
>
>
>
> in response to:
>
>
>
> >>    1.  I'm a little unsure whether the primary
>
> >>    goal is:
>
> >>
>
> >>          (a) To determine whether formal
>
> >>          methods are effectively usable for
>
> >>          IETF-type purposes;
>
> >>
>
> >>          (b) To persuade people that formal
>
> >>          methods are effectively usable for
>
> >>          IETF-type purposes; or
>
> >>
>
> >>          (c) To cause formal methods to become
>
> >>          more effectively usable for IETF-type
>
> >>          purposes.
>
> >>
>
> >>          Of course, a possible response is to
>
> >>          give a blend of more or less of these
>
> >>          three components.  And maybe
>
> >>          additional components?  But what would
>
> >>          be the right characterization?
>
>
>
> What makes this a bit askew is the fact that the
>
> most visible activities -- such as the planned
>
> tutorials at the Nov 4 Prague meeting -- really
>
> seem to me closer to 1(b).
>
>
>
> I guess the tutorial goal is primarily education.
>
> Since formal methods are in fact very useful, one
>
> expects education to be key to "persuading people
>
> that formal methods are effectively usable for
>
> IETF-type purposes."  ( :- )
>
>
>
> And I suspect that persuading and educating may be
>
> a more achievable goal for the UFMRG than actually
>
> causing formal methods to become more effectively
>
> usable.
>
>
>
> That requires instead a lot of research, both with
>
> a high level of insight into formal modeling and
>
> proving, and with a bunch of user studies and
>
> appraising the kinds of people who could benefit
>
> from specific kinds of FM.
>
>
>
> Would the 4 Nov tutorials even give us any insight
>
> into the latter?
>
>
>
> It's conceivable but might require some
>
> coordination and restructuring.
>
>
>
> More on question (2) in a separate msg.  I'd be
>
> eager to know what people think about these
>
> aspects of question (1).
>
>
>
>         Joshua
>
>
>
> On 9/1/23, 12:01, "Stephen Farrell" <stephen.farrell@cs.tcd.ie> wrote:
>
>
>
> 1(c) is fine, 2(c) is closest but not quite right
>
>
>
> On 01/09/2023 16:58, Joshua D Guttman wrote:
>
> > May I ask a few questions about the UFMRG goals?
>
> >
>
> > 1.  I'm a little unsure whether the primary goal
>
> >      is:
>
> >
>
> >      (a) To determine whether formal methods are
>
> >          effectively usable for IETF-type purposes;
>
> >
>
> >      (b) To persuade people that formal methods are
>
> >          effectively usable for IETF-type purposes;
>
> >          or
>
> >
>
> >      (c) To cause formal methods to become more
>
> >          effectively usable for IETF-type purposes.
>
> >
>
> >      Of course, a possible response is to give a
>
> >      blend of more or less of these three
>
> >      components.  And maybe additional components?
>
> >      But what would be the right characterization?
>
> >
>
> > 2.  Along another axis, we sometimes have
>
> >      different formal methods that may be useful
>
> >      for different sets of goals (eg establishing
>
> >      that a program respects an inductive invariant
>
> >      vs establishing that a protocol achieves an
>
> >      authentication goal), and maybe also competing
>
> >      formal methods that approach the same goals in
>
> >      different (or similar :- ) ways.
>
> >
>
> >      Do we aim to:
>
> >
>
> >      (a) Identify some methods as suitable for some
>
> >          kinds of goals?
>
> >
>
> >      (b) Grade the usability of some "competing"
>
> >          methods for overlapping goals?
>
> >
>
> >      (c) Identify combinations of methods for
>
> >          purposes that require several kinds of
>
> >          results?
>
> >
>
> >      Again, blends may make sense together.
>
> >
>
> > Thanks!
>
> >
>
> >    Joshua
>
> >
>
> >
>
>
> --
> Ufmrg mailing list
> Ufmrg@irtf.org
> https://www.irtf.org/mailman/listinfo/ufmrg
>