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

Hi Hans-Dieter,

what chapters of Software Foundations do you suggest reading beforehand?

https://softwarefoundations.cis.upenn.edu/

- Gergely

On Mon, 11 Sept 2023 at 14:06, Hans-Dieter Hiep <hdh=40cwi.nl@dmarc.ietf.org>
wrote:

> 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: +49 351 463-42048
>
> Email: muhammad_usama.sardar@tu-dresden.de
>
> Website:
> https://tu-dresden.de/ing/informatik/sya/se/die-professur/beschaeftigte/muhammad-usama-sardar
>
>
> ------------------------------------------------------------------------------------------------------------------------------------------
>
>
> ------------------------------
> *Von:* Ufmrg <ufmrg-bounces@irtf.org> <ufmrg-bounces@irtf.org> im Auftrag
> von Jonathan Hoyland <jonathan.hoyland@gmail.com>
> <jonathan.hoyland@gmail.com>
> *Gesendet:* Freitag, 8. September 2023 00:27
> *An:* Joshua D Guttman
> *Cc:* Stephen Farrell; ufmrg@ietfa.amsl.com
> *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, <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
>>
>
> --
> Ufmrg mailing list
> Ufmrg@irtf.org
> https://www.irtf.org/mailman/listinfo/ufmrg
>