Xavier Denis

That's already better than a crash!

Hi! Thanks for this proposal, on the broad strokes I'm not against this, but I do have a key question: when do you envision this being useful? What kinds of...

> My initial opinion on this was that Creusot should actually not guarantee the absence of panic, but only try to ensure it as a "best effort". > know that...

> The only thing that might be worth looking at now is the "Reduce code duplication" commit, that's a bit orthogonal to the rest of this but it becomes more...

Something that would be nice especially for these kinds of safe apis would be to actually prove their specs on a re-implementation. These functions typically are 1-2 lines each, and...

:wave: would you like me to take this over?

Indeed, I haven't thought about how to integrate `impl Trait` into Creusot, though I don't think it is necessarily so difficult. What are you expecting to prove? I imagine that...

You can mark functions as `#[trusted]` to tell creusot to skip them. This will still translate the signatures but should be used for parts of the code that can't /...

Yea, this is a notion we have called "deep" vs "shallow" models. @jhjourdan and I have agreed that deep models (`Seq`) are the proper way forward for `Model`, but we'll...

I've significantly weakend the conditions on the invariant of `Map`, but this comes at a cost: the proof of `next` is _extremely_ painful to get to go through, and it...