Sam Stites (Mar 15 2021 at 15:31): Sam Stites (Mar 15 2021 at 15:31):If I wanted to write a small compiler on top of the LLVM using OCaml and verify properties of this language without using a project like vellvm, would I later regret this decision? For context, I'm hoping to write a small array language and prove semantics about APL-like accessors, but I'm a bit concerned about working with floats.
Yannick Zakowski (Mar 15 2021 at 15:38):Hi Sam! Part of me thinks you'll regret it, but I might be biased ;)
It highly depends on what properties you want to verify, and about which components. If you are going to compile toward LLVM IR, and want to reason about the semantics of the code you generate, then I would tend to think that you should join us and use Vellvm :) You will need a semantics for LLVM IR.
If you only want to prove properties of your source language and are happy to trust your compiler, then no need for Vellvm indeed, you should only have to model your source language and reason about it.
Sam Stites (Mar 15 2021 at 15:42):Thank you!
Last updated: May 31 2023 at 09:01 UTC