News for hackers. Stuff that matters.

A comment on AlphaProof Code. Parent comment

Re:AlphaProof Code by viraptor on Tuesday November 10, 2026 @08:21AM (#50439916)
It's not and we don't. We can however run some lean in rust with things like https://github.com/conao3/lean-rs

Or you can use verus instead which does automatic mapping from the rust code to the proof where possible.

[ Parent | on HN ]
Re:AlphaProof Code by Paracompact on Tuesday November 10, 2026 @08:49AM (#50440323)
Not sure why you're responding with information that would imply they modeled Rust in Lean or vice versa. As I explained, their target was the compiled ELF binary, not Rust source. This way, they avoid including the entire Rust compiler and its as-yet formally undefined semantics into the trusted computing base.
[ Parent | on HN ]