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

[Hans-Dieter Hiep <[e-mail]>]

Hi Usama,


The Coq training we will be giving will be tailored to 
intermediate-level Coq users, but beginners and experts are of course 
also welcome. We will already make some material available on-line in 
one month to allow attendees to prepare, and we expect the audience to 
have already some experience with the basics of Coq (but still go over 
it quicktly; we can spend most time on intermediate-level proving). The 
training is not reused, it's designed from scratch by me and Dalia in 
the coming weeks. If there are any suggestions, please let me know.


Kind regards, Hans-Dieter


On 9/8/23 09:45, Muhammad Usama Sardar wrote:
>
> Hi Joshua,
>
> Thanks for your questions. I think they are very good points. Until 
> this thread, I was under the impression of 1(b) as well.
>
>
> If the main goal is 1(c), then improving the manuals of tools should 
> be an equally (if not more) important activity. Let's face it: we all 
> know how poorly most (if not all) of these manuals are documented.
>
>
> > 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.
>
> I don't think this was explicitly clarified before to the volunteers. 
> Some questions in my mind are:
>
>   * Are the trainers now aware that they are supposed to give
>     intermediate level training and not repeat what they have already
>     presented elsewhere?
>   * Is it still feasible for them to create this intermediate level
>     training within the next 2 months?
>   * Are you certain that you will get enough people in the audience
>     interested in intermediate level training (i.e., well-aware of the
>     basics of the tools)?
>
>
> Thanks,
>
> Usama
>
>
> ------------------------------------------------------------------------------------------------------------------------------------------
> Best Regards,
>
> Muhammad Usama Sardar (M.Sc.)
>
> Research Associate
>
> Technische Universität Dresden
>
>
> Faculty of Computer Science
>
> Institute of Systems Architecture
>
> Chair of Systems Engineering
>
>
> Office: APB 3073
>
> Phone: [phone]
>
> Email: [e-mail]
>
> Website: 
> https://tu-dresden.de/ing/informatik/sya/se/die-professur/beschaeftigte/muhammad-usama-sardar 
> <https://tu-dresden.de/ing/informatik/sya/se/die-professur/beschaeftigte/muhammad-usama-sardar>
>
> ------------------------------------------------------------------------------------------------------------------------------------------
>
>
>
> ------------------------------------------------------------------------
> *Von:* Ufmrg <[e-mail]> im Auftrag von Jonathan Hoyland 
> <[e-mail]>
> *Gesendet:* Freitag, 8. September 2023 00:27
> *An:* Joshua D Guttman
> *Cc:* Stephen Farrell; [e-mail]
> *Betreff:* 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, <[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
>
>     >
>
>     >
>
>     -- 
>     Ufmrg mailing list
>     [e-mail]
>     https://www.irtf.org/mailman/listinfo/ufmrg
>
>