[Verifpal] (feature request) Consistent case sensitivity

[Nadim Kobeissi]

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