Hacker News Reader

Comment by agentultra | Hacker News Reader

A nicely written article! And an interesting project.

Myself, I'd lean towards a sound (linear) type theory. If it's not too much trouble, insert the run-time checks in debug builds but use the type system to erase them for optimized builds. It might seem like the mountain is impossible to climb if you're not used to formalizing such systems but every mountain is surmounted one step at a time.

It's hard to bolt-on correctness after the fact. In my experience, for critical pieces like this, it's better to get the specification right first before digging in too deep and writing code.

Best of luck on the project either way you go. Memory safety is increasingly important!

View on HN

Although linear typing is certainly interesting, I think linear typing on its own is not enough. That is, you basically end up with something like Austral where you use linear types _plus_ some form of compile-time borrow checking, at which point we're back at borrow checking (did I mention it seems inevitable?) :)

You did! And maybe it is inevitable? I don't know.

It'd be interesting to see different theories evolve, for sure. Maybe something in separation logic will make it's way into mainstream type theory and into compilers at some point.

What's cool is how much we're starting to see folks push the boundaries these days. :)

Wouldn't the borrow checking be simpler when built on top of linear types?

I don't think the choice of linear vs affine makes much of a difference, but I could be mistaken.

I think a real challenge with trying to work on specifications first is error handling -- you often find that a truly sound model is quite difficult to explain to users. So some prototyping and iteration becomes necessary in my experience.

Like, rustc only recently gained the ability to explain that the borrow checker rejected a program because a lifetime parameter was invariant. And this isn't even an artificial bit of complexity -- if you have mutability you are required to think about variance. If you have a Cell<&'static str> you cannot just turn that into a Cell<&'a str>, the way you can turn a regular &'static str into a &'a str. (Java programmers might be familiar with similar issues around ArrayList<Object>.)

Reply on news.ycombinator.com