-
Notifications
You must be signed in to change notification settings - Fork 14
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
interest in isabelle backend? #284
Comments
Sorry for my (very) late answer: I got busy with other things then went to vacations. Generally speaking, we are interested in having backends, in particular a backend for Isabelle, but if people need and use them (for instance they're doing a verification project with the backend) and are ready to maintain them, because on our side this is a lot of work. |
fair — I don't currently have much of a project for which I'd be ready to maintain this backend; should that change I might yet start with that though (of if anyone else is reading this & might be interested in using aeneas with Isabelle, feel free to reach out!)
do I understand this correctly as, associated types will become parameters of the trait itself (instead of fields inside its dictionary-structure), and at use-sites they are resolved by charon already? That would be neat for Isabelle (can't promise I'll look at it again/implement this, but perhaps if I have the time) |
Yes, this is exactly what we intend to do. As a side note: if you're interested in contributing and learning Lean, there is a lot to do on the Lean backend (including: adding definitions to the standard library, writing and verifying examples to exerce the backend, implementing better automation, etc.). :) |
Hi all! @RaitoBezarius pointed me here a while ago. Originally I was interested in using aeneas to maybe try and verify some of my own rust code (& finally actually use Lean while doing it), but I soon got distracted by that sentence from the readme — and well, having played with Isabelle/HOL things in the past, I accidentally nerdsniped myself into writing the basic parts of such a backend.
The current diff is here: main...stuebinm:aeneas:isabelle
Current state: it can produce valid Isabelle functions for most simple struct/enum declarations & terms, as long as they do not make any kind of use of traits (as a test case, I used a simplified version of the avl tree verification with uses of traits removed). There's not much testing yet though, so it's very possible to get it to generate invalid code. The primitives lib for Isabelle is also as basic as it can possibly be for the avl tree example (it contains nothing but a
u32
type and a less-than operator on it).Unfortunately I'm not sure how feasible real support for rust's traits in the translation is — while simple traits should easily map to either a reified datatype representation or to Isabelle's own type class system, I don't see any obvious way to have support for associated types in traits (as in Isabelle, types and values are very much distinct things). I've looked into the HOL4 backend a little since I suspect (although i don't know much of HOL4) it has the same issue, and afaict it seems to always fail if associated types are present as well?
I'm opening this issue mostly to ask how much interest you have in an Isabelle/HOL backend overall / if you'd have any use for my code — for me this is currently a pure hobby project, and while I might continue on it until it's a (very little) bit closer to feature-complete I don't really intend to maintain it on my own in the long term.
The text was updated successfully, but these errors were encountered: