Hax playground: translate Rust to proof assistants, now online

announcements
1

hax is a tool that translates a large subset of Rust into formal languages such as F* or Coq.

Today we're announcing our playground, which allows playing with hax directly from your browser!

From there, you can translate your Rust code to formal languages, share snippets of code, and try to formally verify code with the F* prover.

The hax toolchain ships with a frontend and a custom rustc driver: they expose hax' very own version of THIR and MIR Rust abstract syntax trees. Those THIR and MIR are plain trees, where no interactive queries to rustc are required. Our frontend is used by hax but also by Charon/Aeneas, another verification toolchain.
On the playground, right-clicking on a Rust expression will allow you to browse the THIR or MIR ASTs interactively, try it out!

Check out our blog post, which gives more details!

Feel free to try it out and give us feedback!

4 Likes
2

Unfortunately, it doesn't seem to work. The pre-loaded example never finishes compiling, it says "query sent, waiting for response" forever.

3

Oh, that's odd, it might be a browser incompatibility. What is your configuration, what operating system & browser are you on?

4

I'm on Mobile Safari on iOS 16. Indeed a mobile browser may not be the ideal condition for such a UI-heavy project, although the regular Rust playground does work on mobile, so I though I'd give this one a try while on my way.

5

Ok, thanks for the feedback, I found what was the bug, it's now fixed, it should work :slight_smile:

1 Like
6

Yes, it does indeed work now, thanks!

1 Like
7

This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.