4 ms·
Let's say you are using LLVM to compile a Rust program, and an "equivalent" C program. You can compile both of them down to IR, and then enforce type safety at
by dronemallone 9y ago
Let's say you are using LLVM to compile a Rust program, and an "equivalent" C program. You can compile both of them down to IR, and then enforce type safety at the IR level. Doesn't that ensure that you can prove properties about the program at compile time?
- projektir 9y agoThe hard part is getting the "equivalent" C program. :)
- eridius 9y agoYou can't enforce type safety at the IR level. LLVM IR has very little in the way of type information.
- nonsince 9y agoI've been manually writing some LLVM IR recently to prepare for a project involving JIT compilation, and LLVM's type system is actually shockingly expressive. The majority of the problems I run into are the fact that you have to copy-paste more often and that leads to errors. I wouldn't recommend anyone write real code using LLVM IR, but it's not as bad as you'd expect.
- deleted 9y ago[deleted]
- proyb2 9y agoJust to the same links to your question. https://gcc.godbolt.org https://gcc.godbolt.org https://rust.godbolt.org https://rust.godbolt.org
- joshuata 9y agoPossibly, but types can encode far more than just the structure of data. Rust, for example, uses types to encode lifetime and ownership information. Haskell uses the IO monad to encapsulate non-determinism. Neither of those have equivalent concepts at the IR level. It's not a set law, but more expressive type systems almost always increase the class of properties that can be "easily" proved in a language. I work on a verification tool for C/C++ programs and we constantly struggle with the languages. Pointer arithmetic and aliasing dramatically complicate any possible analysis, and these problems are only exacerbated at a lower level IR/ASM level.