Brian Hicks (Nov 07 2022 at 14:51): Brian Hicks (Nov 07 2022 at 14:51):would it be possible to test Roc programs using Crux? Their intro blog post says it can analyze LLVM code!
(summary of what Crux is: it provides symbolic verification so you can do things like saying "for all x: u32, x + 1 > x". It'll then find u32::MAX and say "but what about this one?" I think there are more complex/interesting examples on their website at https://crux.galois.com/)
Brian Hicks (Nov 07 2022 at 14:51):oops, intro blog post ist at https://galois.com/blog/2020/10/crux-introducing-our-new-open-source-tool-for-software-verification/
Ayaz Hafiz (Nov 07 2022 at 14:57):I think you certainly could, though they may expect IR invariants that Roc does not preserve (our lowering to LLVM IR transforms to something that is very far away from the source code)
Ayaz Hafiz (Nov 07 2022 at 14:57):for IR level symbolic execution there is also http://klee.github.io/
Ayaz Hafiz (Nov 07 2022 at 15:00):A language like Roc should have a pretty easy time embedding into a solver or proof assistant from the source language though, so that could also be promising
Kevin Gillette (Nov 07 2022 at 15:01):From the source language, i.e. AST?
Ayaz Hafiz (Nov 07 2022 at 15:01):AST + types yeah
Kevin Gillette (Nov 07 2022 at 15:08):I'm guessing the Roc frontend to LLVM does some Roc-specific optimizations before it produces IR? If so, would the resulting IR still have reasonable usability for IR-based tools?
Would producing non-optimized IR (to simplify proof-writing) prove anything meaningful about how the optimized IR behaves? Would proofs based on AST + types have implicit coverage over the IR as well? I suspect all of the above could still catch soundness issues, but I wonder if any approach alone would cover well both the language and compiler?
Ayaz Hafiz (Nov 07 2022 at 15:12):Would producing non-optimized IR (to simplify proof-writing) prove anything meaningful about how the optimized IR behaves?
It could, but there is probably more value in doing this for user code rather than the compiler - verifying the compiler is useful but there are other ways to do that.
For that reason extracting theorems (and proofs) from Roc source code is probably more viable, because Roc's compilation to LLVM IR is not (really) source preserving, and differs in complexity significantly (our LLVM IR has no higher-order constructs, but Roc programs are full of them)
Last updated: Jun 16 2026 at 16:19 UTC