Rename equality operators

[Lysxia]

I think we should

1. rename == to ===,
2. define x == y as x.deep_model() === y.deep_model() so that it matches the Rust function.

I like === because it's "more equals" than == and it's like Javascript which is a very successful language.

[xldenis]

I wouldn't say that equality is considered one of JavaScripts strong points though :p

[dianegolfouse]

One thing I don't like about this is that it would require using pearlite! in even more places... At this point we could just force every #[logic] function to wrap its body in pearlite!

[xldenis]

Unfortunately that's not possible since attribute macros require their subject to be a valid rust expression. In fact that's one of the reasons we dropped === (which was used early in creusot)

[Lysxia]

Maybe we could wrap multiple logic functions in pearlite! (or some other decl macro).

pearlite! {
  fn blah() { blah }
}
// expands to
#[logic]
fn blah() { pearlite!{ blah } }

[xldenis]

yeah you can but then you lose autocompletion, formatting etc...

[xldenis]

my dream would be to kill pearlite! and use exclusively valid rust syntax. it would play a lot nicer with rust tooling / infra.

[jhjourdan]

Perhaps we can give a bit more context here: @Lysxia did a Creusot tutorial to NVidia people, and the fact that == had a different semantics in Pearlite and in Rust was something they criticized, arguing that this is confusing to new users. Also, the fact that we need to put a lot of @ everywhere was a source of complains.

With this proposal, we answer fully the first criticism, and partially the second one (because == would apply deep_model implicitly).

Unfortunately that's not possible since attribute macros require their subject to be a valid rust expression.

Pearlite expressions are anyways not valid Rust syntax. pearlite! is needed in many cases. And there is at least one case where I think we don't want to go to a Rust-compatible syntax because it's going to make it much more heavy and asymmetric: the ^ prophecy operator.

[xldenis]

Yeah the differing semantics of == is definitely a problem but I don't find ^ all that convincing: it's a frequent source of complaints as well. I really think the value of not using pearlite! can be understated from a ux perspective either.

[jhjourdan]

it's a frequent source of complaints as well.

Are the complaints about the syntax or rather about the concept of prophecy? Can you think of a syntax which would ne be really worse?

[xldenis]

The syntax. People complain that creusot "doesn't have a rust syntax", this has been used specifically in reference to ^ and to quantified syntax.

[dianegolfouse]

Note that using a single = produces valid Rust syntax (see https://doc.rust-lang.org/stable/reference/expressions/operator-expr.html#assignment-expressions). I'm not quite sure we want to take advantage of it, but its possible.

[jhjourdan]

Good point. I think we did not use that because it is confusing with the = syntax of let bindings, and because it can be confusing for Rust user who use to think of = as assignment.

Another problematic point is that it does not have the right precedence wrt. && and ||. If we use a different precedence that Rust uses, then there will be no hope of using Rust tooling for indentation and so on.

[Lysxia]

Maybe we can find a way to overload == satisfactorily. I strongly think that the "equivalence relation" interpretation should be the default, so the question is what extra syntax will indicate the other choice "physical equality":

1. A qualifier on an argument, like x == y.exactly()
2. A qualifier around the equality, like exactly(x == y), #[exact_equality] x == y
3. A qualifier/attribute that changes the interpretation of == in a whole scope, exactly(x == y && forall<t> f(t) == u), #[exact_equality] { x == y && forall<t> f(t) == u }

[Lysxia]

A separate question. In cases where deep_model is defined as the identity function, notably for machine integers and other "plain" types, you'd like to just write x == y because it's shorter. Is it important that it translates to x = y in Why3 rather than deep_model x = deep_model y? I feel like "industrial" SMT solvers should handle that difference effortlessly, but do they?