Don't fall into the anti-AI hype

Re:Don't fall into the anti-AI hype by eru on Monday January 12, 2026 @01:49AM (#46584963)

> Haha. How do you reconcile a proof with actual code?

You can either proof your Rust code correct, or you can use a proof system that allows you to extract executable code from the proofs. Both approaches have been done in practice.

Or what do you mean?

[ Parent | on HN ]

Re:Don't fall into the anti-AI hype by thesz on Monday January 12, 2026 @01:42PM (#46592471)

Rust code can have arbitrary I/O effects in any parts of it. This precludes using only Rust's type system to make sure code does what spec said.

The most successful formally proven project I know, seL4 [1], did not extracted executable code from the proof. They created a prototype in Haskell, mapped (by hand) it to Isabelle, I believe, to have a formal proof and then recreated code in C, again, manually.

[1] https://sel4.systems/

Not many formal proof systems can extract executable C source.

[ Parent | on HN ]