Clément Blaudeau

Some code produce errors in the engine, but those errors are not printed properly. See for instance : ```rust fn f() { loop {} } ``` [Open this code snippet...

Currently, the Lean backend assumes that the order on the items is compatible with the dependencies, both at top-level and within traits/impls. Therefore, it will produce invalid code when faced...

The `Result` monad used in the Lean backend is confusingly named the same as the Result type of Rust. We should change the former to something not used in Rust...

Currently, the Lean backend only support "basic" pattern-matching : wild patterns, constructors, or-patterns. It should also support matching on: - [ ] Arrays - [ ] Constants - [ ]...

So far, the Lean backend does not support variables captured by closures.

[Lean] Arrays with non-integer-literal size

1

Currently, the Lean Backend only supports arrays where the size is an integer literal. This was done to avoid issues of type equality between types like `Vector Nat 5` and...

Compare Rust verification tools

3

There are many rust verification tools being developed, with different use-cases and features. It would be very useful to do the zoology of rust tools, i.e. to understand their defining...

```rust fn f( x: u8) -> u8 { ({ let x = 9 ; 0 }) + x } ``` [Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/latest-main/gist=8adb631136cedbf401277d07075ae5db) The hax engine...

[Lean] Extend support for associated types

1

Currently, the Lean Backend only support trait-local associated types, and no equality constraints (called generic projection constraints).