Wow that was very interesting to read and shows you guys are pushing boundaries even when the goal is a pragmatic language.
One last big thing that Shapiro mentioned was criticizing purity alone as a useful way of attacking concurrency and losing faith in verification. Can you or someone else knowledgeable comment on this?
>The last reason we left objects out of BitC initially was purity. I wanted to preserve a powerful, pure subset language - again to ease verification.
The object languages that I knew about at the time were heavily stateful,
and I couldn't envision how to do a non-imperative object-oriented
language. Actually, I'm still not sure I can see how to do that
practically for the kinds of applications that are of interest for BitC.
But as our faith in the value of verification declined, my personal
willingness to remain restricted by purity for the sake of verification
decayed quickly.
The other argument for a pure subset language has to do with advancing
concurrency, but as I really started to dig in to concurrency support in
BitC, I came increasingly to the view that this approach to concurrency
isn't a good match for the type of concurrent problems that people are
actually trying to solve, and that the needs and uses for non-mutable state
in practice are a lot more nuanced than the pure programming approach can
address. Pure subprograms clearly play an important role, but they aren't
enough.
Sure. Regarding concurrency, we're trying to eliminate data races by avoiding shared mutable state. Right now, our unique pointers attack the "shared" part of that -- since data in the exchange heap is localized to a single task, you don't have data races, regardless of mutability. So mutable structures aren't a concern there.
There is the concern that unique pointers are too limited to do a lot of the kind of tasks you want to do in a parallel way, and that's where the experiments we want to do with the "patient parent" model come in -- you can see my colleague Niko's blog here [1] for info on that. That approach allows shared immutable data.
Verification has never been a goal of ours, except for the kinds of invariants you can address relatively simply in a type system. Dependent types are cool, but at the moment they're so complicated as to place the language out of reach of most programmers. We have more interest in making dynamic checks (assertions, design-by-contract) easy to use.
One last big thing that Shapiro mentioned was criticizing purity alone as a useful way of attacking concurrency and losing faith in verification. Can you or someone else knowledgeable comment on this?
>The last reason we left objects out of BitC initially was purity. I wanted to preserve a powerful, pure subset language - again to ease verification. The object languages that I knew about at the time were heavily stateful, and I couldn't envision how to do a non-imperative object-oriented language. Actually, I'm still not sure I can see how to do that practically for the kinds of applications that are of interest for BitC. But as our faith in the value of verification declined, my personal willingness to remain restricted by purity for the sake of verification decayed quickly.
The other argument for a pure subset language has to do with advancing concurrency, but as I really started to dig in to concurrency support in BitC, I came increasingly to the view that this approach to concurrency isn't a good match for the type of concurrent problems that people are actually trying to solve, and that the needs and uses for non-mutable state in practice are a lot more nuanced than the pure programming approach can address. Pure subprograms clearly play an important role, but they aren't enough.
And I still don't believe in monads. :-)