David Ewert

We would probably want an extern spec for `::core::hint::unreachable_unchecked()` (requires false) as a building block. This would be useful on its own (for example when pattern matching) and could also...

I just check and it is, I'm not sure where/if this is documented, I usually just look at `creusot-contracts` to see what is supported

Now that #488 has been merged this seems to have become a soundness issue. However, I'm not sure it would be okay to make logic functions forbidden in ghost code...

Thanks for your quick responses. I've been playing around with a few things including a form of aliasing where one pointer is the primary and other pointers can read/write if...

> Any functions in particular? This is something I need to work on more again. I started by implementing `fold` with a desugared for loop and now am trying to...

Thanks, @rrbutani for providing the explanations and examples, I think with these I can close this issue. As for other receiver types, I think it might be worth adding if...

I've been exploring the idea of using `'static` as an erased lifetime myself, and I came up with something that seems reasonable to me: [dewert99/erased_brand](https://github.com/dewert99/erased_brand). Is there any unsoundness with...

OddTheory: ```rust use std::ops::{Deref, DerefMut}; use batsat::{Lit, Theory, TheoryArg}; #[derive(Default)] pub struct OddTheory(pub Th); impl Theory for OddTheory { fn final_check(&mut self, acts: &mut TheoryArg) { self.0.final_check(acts) } fn create_level(&mut...

> We hope that anyone with a good use case for keeping the status quo will speak up, because so far we've only been able to create artificial examples I...

> This is definitely not true. Cell::get will be a const fn eventually. Hmm, if `Cell::get` can become a `const fn`, then the other const-eval restrictions seem less useful. >...