Ask HN: Can we translate normal Rust (axum) to Lean 4 without restrictions?

Original Summary

I'm trying to build a web app in Rust using axum, and am thinking whether I can export that Rust code to Lean4 so that I can verify business logic or security properties.I first tried Aeneas, but it can only work for restricted grammer and structurs that are hard to review (it even doesnt look like Rust).For example, when I want to write:`` fn find_post(ps: &[Post], id: u64) -> Option<&Post> { ps.iter().find(|p| p.id == id) } `I have to write:` pub fn find_post(ps: &Vec<Post>, id: u64) -> Option<Post> { let mut i = 0; while i < ps.len() { if ps[i].id == id { return Some(ps[i].clone()); } i += 1; } None } ``Is there anybody who have addressed this kind of problem??For anyone interested, the experiment source and examples are at https://github.com/h5i-dev/i5h. I've ported parts of a few real web apps (e.g., Kellnr, Atuin, Wastebin, Conduit), and their core logic can now be verified to some extent. Ofcourse, that does assume the rest is correct, like axum/hyper for HTTP and PostgreSQL plus the engine for storage.

情报分类：商业与市场研究
分类依据：内容涉及商业、投资或市场动态
信息来源：Hacker News 新项目
发布时间：2026/9/29 00:42:59

Original Summary

发表回复