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

[Nadim Kobeissi <[e-mail]>]

For what it's worth, what Jonathan is saying matches my observations.

Both Tamarin and ProVerif stand to gain from soemone working full-time
on improving web interfaces, better error messages, better tooling and
integration...

However, academic incentives lie elsewhere.

-- 
Nadim Kobeissi
Symbolic Software - https://symbolic.software

On Thu, 2023-09-07 at 23:27 +0100, Jonathan Hoyland wrote:
> 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, <[e-mail]>
> 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" <[e-mail]>
> > 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
> > > 
> > > 
> >