[Verifpal] (feature request) Consistent case sensitivity

[Loup Vaillant David]

That's settled, then. Good.

Would you be willing to consider adding (or accept a patch that adds)
warnings about inconsistent casing, such as using both "FOO" and "foo"?

Loup.


On Sun, 2019-09-01 at 10:18 +0200, Nadim Kobeissi wrote:
> Dear Loup,
> 
> Thanks for raising this valid point. Despite your valid arguments,
> I’m personally very much in favor of moving towards full case
> insensitivity, because I think that this will make it harder for
> undergraduate students to make errors when using Verifpal. This is
> because goal 2 of Verifpal’s four main goals is "Modeling that avoids
> user error.”
> 
> I am pretty opinionated on this, and barring any hugely important
> arguments I don’t think I will change my mind. I hope the reason is
> clear. Happy to continue the discussion, however.
> 
> I’ll move the code more clearly in this direction in the coming
> weeks.
> 
> Have a great start of the academic year,
> 
> Nadim Kobeissi
> Symbolic Software • https://symbolic.software
> 
> > On Aug 30, 2019, at 7:52 PM, Loup Vaillant David <
> > loup at loup-vaillant.fr> wrote:
> > 
> > Hi,
> > 
> > Yet another nice to have, quality of life suggestion. This one is
> > quite
> > bikeshed-y, and I'm not even sure what's the best solution myself
> > (I
> > just have my personal preferences). You may want to just make a
> > call
> > and stick to it.
> > 
> > ---
> > 
> > I noticed that Verifpal is *partially* case insensitive:
> > 
> > - Constant identifiers are case insensitive.
> > - Primitive names are case insensitive.
> > - Keywords (principal, attacker…) seem to be case *sensitive*.
> > 
> > I didn't like the inconsistency. If you want case insensitivity,
> > *everything* should be case insensitive. I think. Maybe. In any
> > case,
> > this got me thinking. There are basically 3 possible policies:
> > 
> > - Case sensitive.
> > - Case insensitive.
> > - Case "consistent" (a paranoid version of case insensitivity).
> > 
> > My personal preference is case sensitivity, for two reasons: first,
> > if
> > you accept unicode characters, case insensitivity is locale
> > sensitive.
> > Take "i" and "I" for instance. In English, the lower case one is
> > dotted, the upper case one is not. In Turkish however, there's a
> > real
> > difference between the dotted "i" and the non-dotted one.  Changing
> > the
> > case of an "i" in Turkish preserves the (lack of) dot! I see only 3
> > ways out of this nightmare: forbid unicode characters, assume an
> > English locale, or give up and become case insensitive.
> > 
> > The second reason is more serious: there's this convension where we
> > give the same name to both halves of a key pair: (ak, AK). By
> > convention, the lower case half "ak" represent the private key, and
> > the
> > uppercase half "AK" represents the public key. I personally like
> > this
> > convention, and use it when generating Monokex specifications. I
> > can't
> > do the same with Verifpal however, because its identifiers are case
> > insensitive.
> > 
> > Now there are valid reason to still prefer case insensitivity my
> > beloved convention be dammed. But then there's a tweak that might
> > help
> > readability: once we have chosen a case, we have to *stick to it*.
> > For
> > instance, the following would fail:
> > 
> >    principal Alice [
> >        knows public FOO
> >    ]
> >    principal Bob [
> > 
> > knows public foo
> >    ]
> > 
> >  Syntax error: same identifier with different casings: "FOO", "foo"
> > 
> > That way the casual reader would not be left wondering whether
> > "FOO",
> > "foo", or "Foo" refer to different things: once you've passed
> > Verifpal,
> > it would not even matter to the reader whether that thing is case
> > sensitive or not.
> > 
> > Now there's nothing urgent about the colour of that bike shed. When
> > we
> > polish for 1.0 however, this might be worth thinking about.
> > 
> > Loup.
> > 
> > 
> > 
> > _______________________________________________
> > Verifpal mailing list
> > Verifpal at lists.symbolic.software
> > https://lists.symbolic.software/mailman/listinfo/verifpal
> 
>