Сухарик

By the way, the ability to use functions in refinements is not documented. https://flux-rs.github.io/flux/guide/specs.html#grammar-of-refinements does not mention lambdas.

Why3 documentation says that Coq must be installed before building Why3: > If you want to use the Coq realizations ([Section 10.2](https://www.why3.org/doc/itp.html#sec-realizations)), then Coq has to be installed before Why3....

I see, thanks. Though `opam install --switch ~/.local/share/creusot why3-coq` does not work, because it requires why3

I guess I need to patch `creusot-deps.opam`, so it does not use git versions of packages for which there's no `why3-coq` version.

> And a final remark: it is true that Why3 currently does not offer Lean as a back-end, but we would certainly be happy to accept patches to make it...

An idea: https://www.osar.fr/protoplug/ It's not maintained anymore though. But Lua is still a popular scripting language. > so I was thinking about a lightweight Lisp-like DSL If you're going to...

> Lisp seems quite complex from what I see on Wikipedia France... Scheme is actually a pretty simple language. Look at the standard, it's tiny compared to many other standards:...

I would like if someone else maintained this package. > Maybe I can try packaging for NixOS but I don't know much about that. Since there's already a package, you...

It seems like my involvement was not required to update the package: https://github.com/NixOS/nixpkgs/pull/336821

I was able to build it and run nonetheless.