Merge pull request #1546 from cryspen/this-month-in-hax-june-2025

This month in hax June 2025.

Author: franziskuskiefer

docs/blog/posts/this-month-in-hax/2025-06.md

@@ -0,0 +1,48 @@
+---
+authors:
+  - maxime
+title: "This Month in Hax: June 2025"
+date: 2025-06-08
+---
+
+In June, we successfully merged **21 pull requests**!
+
+[@Nadrieril](https://github.com/Nadrieril) and [@N1ark](https://github.com/N1ark) continued the improvements on the frontend side with the addition of unchecked arithmetic operators ([#1513](https://github.com/cryspen/hax/pull/1513)), regrouping generic and trait arguments in a struct ([#1514](https://github.com/cryspen/hax/pull/1514)), support of trait aliases in `full_def` ([#1494](https://github.com/cryspen/hax/pull/1494)), addition of `Ty::FnDef` ([#1487](https://github.com/cryspen/hax/pull/1487)), drop calls resolution ([#1467](https://github.com/cryspen/hax/pull/1467)) and more.
+
+[@W95Psp](https://github.com/W95Psp), [@clementblaudeau](https://github.com/clementblaudeau) and myself worked on adding infrastructure for writing backends and compilation phases for hax in Rust (instead of Ocaml). We now have a Rust version of the hax AST and we can convert back and forth from the Ocaml version (which should allow to incrementally replace Ocaml phases by Rust phases). We also offer utilities for printing this AST when implementing backends. Our plan for the next months is to use this for the new backends we will add, and experiment with Rust phases.
+
+Stay tuned for more updates next month!
+
+### Full list of PRs
+
+* \#1517: [Update charon.yml: add `workflow_dispatch`](https://github.com/cryspen/hax/pull/1517)
+* \#1514: [Regroup generic and trait arguments in a struct](https://github.com/cryspen/hax/pull/1514)
+* \#1513: [Separate `{Add,Sub,Mul}Unchecked`](https://github.com/cryspen/hax/pull/1513)
+* \#1510: [Fix following merges changing the frontend AST](https://github.com/cryspen/hax/pull/1510)
+* \#1507: [Rust Engine: rename rust printer to rust engine](https://github.com/cryspen/hax/pull/1507)
+* \#1506: [Rust engine: Add spans to the Rust AST.](https://github.com/cryspen/hax/pull/1506)
+* \#1505: [Rust Engine: OCaml bridge for the AST (OCaml AST -> Rust AST)](https://github.com/cryspen/hax/pull/1505)
+* \#1504: [Rust Engine: transport the Rust AST to OCaml](https://github.com/cryspen/hax/pull/1504)
+* \#1502: [Upstream: Rust engine ast](https://github.com/cryspen/hax/pull/1502)
+* \#1501: [Upstream evit changes up to May 19th](https://github.com/cryspen/hax/pull/1501)
+* \#1499: [docs: Escape "*" in "F*" from Markdown](https://github.com/cryspen/hax/pull/1499)
+* \#1494: [full_def: support trait aliases](https://github.com/cryspen/hax/pull/1494)
+* \#1492: [sha256 example typecheck in f*](https://github.com/cryspen/hax/pull/1492)
+* \#1491: [This month in hax May 2025.](https://github.com/cryspen/hax/pull/1491)
+* \#1490: [proof-lib/fstar Add an actual instance for ordering of bound integers](https://github.com/cryspen/hax/pull/1490)
+* \#1487: [Add `Ty::FnDef`](https://github.com/cryspen/hax/pull/1487)
+* \#1485: [Fix detection of trait associated constants](https://github.com/cryspen/hax/pull/1485)
+* \#1482: [Update rustc pin](https://github.com/cryspen/hax/pull/1482)
+* \#1480: [Upstream evit changes up to April 25](https://github.com/cryspen/hax/pull/1480)
+* \#1470: [Add enum coverage test for coq](https://github.com/cryspen/hax/pull/1470)
+* \#1467: [Resolve Drop calls](https://github.com/cryspen/hax/pull/1467)
+
+### Contributors
+* [@N1ark](https://github.com/N1ark)
+* [@Nadrieril](https://github.com/Nadrieril)
+* [@W95Psp](https://github.com/W95Psp)
+* [@chrysn](https://github.com/chrysn)
+* [@clementblaudeau](https://github.com/clementblaudeau)
+* [@cmester0](https://github.com/cmester0)
+* [@karthikbhargavan](https://github.com/karthikbhargavan)
+* [@maximebuyse](https://github.com/maximebuyse)