Hacker News Reader

Comment by joshuata | Hacker News Reader

It might be able to, but there are no guarantees. That is the real benefit of strong and expressive type systems: It can prove properties of the program at compile time. An equivalent program could be written in c, brainf*ck, or even a Turing machine, but it gets harder and harder to prove properties like memory safety the less structured the language.

View on HN

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?

The hard part is getting the "equivalent" C program. :)

You can't enforce type safety at the IR level. LLVM IR has very little in the way of type information.

I'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.

Just to the same links to your question.

https://gcc.godbolt.org https://rust.godbolt.org

Possibly, 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.

Reply on news.ycombinator.com