[Verifpal] (feature request) Consistent case sensitivity

[Nadim Kobeissi]

Yes, but please describe your patch in more accurate technical detail here first (just a few bullet points, preferably with exactly which parts of the language you would be checking for casing, etc. etc.) and wait for my approval before expending your valuable time and effort on it.

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

> On Sep 1, 2019, at 2:59 PM, Loup Vaillant David <loup at loup-vaillant.fr> wrote:
> 
> 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
>> 
>> 
>