4 ms·

I'm personally unfamiliar with the languages you mention in the first paragraph. Would you mind linking to some information about them?

by wvyar 14y ago

mietek 14y ago
BitC could be one of them. Unfortunately, the author has recently announced he's ceasing work on it. 1. http://www.bitc-lang.org/ http://www.bitc-lang.org/ 2. http://en.wikipedia.org/wiki/BitC http://en.wikipedia.org/wiki/BitC
- fusiongyro 14y ago
  He quit because he found type classes to be both insufficient and a lot of trouble for this purpose. My impression is that he would love to work on a new language targeting the same problem but making some different engineering tradeoffs. I hope he manages to secure funding so he can do that, BitC was a very interesting project.
jerf 14y ago
There's a whole range of passes being made at this. I think the last ten years have been about the interpreted "scripting" languages and it's become obvious the next major PL niche is one of these safer-yet-systems-level languages, so in addition to the ongoing research it seems to me like there's been a burst of work on these, with more to come. D is among the most mature, and the least revolutionary, with all that entails. Mozilla is doing Rust. Go arguably fits into this area, though I'm not sure it's quite meant for kernels per se. (It is a systems level language, though.) But given that 2040 was the year tossed in, I was also thinking the next generation after that, where some of the next-next generation of verification would be folded in. There you're looking at Haskell as being the gateway into that world (even though it is not really that verifiable in the strongest sense itself, it gets your foot in the door), and the Coq and Agda and the slowly-but-surely increasingly usable proof assistants, which would be useful for a provable-not-corruptable (via normal software means) software kernel. Though... if one looks at the rate of advance in kernels over the past 30 years and then project out to the next 30, we get a distressingly high probability of it still being in C. Still, I cautiously optimistically (or pessimistically, depending) think that the hardware revolution that we are still only at the beginning of as we run out of Moore's Law is going to produce non-C languages that will eventually be irresistible to produce kernels in. There's going to be ever more constraints we want to maintain and it's going to get harder and harder to maintain them without some sort of language support beyond what C can supply.

I'm personally unfamiliar with the languages you mention in the first paragraph. Would you mind linking to some information about them?

by wvyar 14y ago

I'm personally unfamiliar with the languages you mention in the first paragraph. Would you mind linking to some information about them?

mietek 14y ago

BitC could be one of them. Unfortunately, the author has recently announced he's ceasing work on it. 1. http://www.bitc-lang.org/ http://www.bitc-lang.org/ 2. http://en.wikipedia.org/wiki/BitC http://en.wikipedia.org/wiki/BitC

fusiongyro 14y ago
He quit because he found type classes to be both insufficient and a lot of trouble for this purpose. My impression is that he would love to work on a new language targeting the same problem but making some different engineering tradeoffs. I hope he manages to secure funding so he can do that, BitC was a very interesting project.

jerf 14y ago

There's a whole range of passes being made at this. I think the last ten years have been about the interpreted "scripting" languages and it's become obvious the next major PL niche is one of these safer-yet-systems-level languages, so in addition to the ongoing research it seems to me like there's been a burst of work on these, with more to come. D is among the most mature, and the least revolutionary, with all that entails. Mozilla is doing Rust. Go arguably fits into this area, though I'm not sure it's quite meant for kernels per se. (It is a systems level language, though.) But given that 2040 was the year tossed in, I was also thinking the next generation after that, where some of the next-next generation of verification would be folded in. There you're looking at Haskell as being the gateway into that world (even though it is not really that verifiable in the strongest sense itself, it gets your foot in the door), and the Coq and Agda and the slowly-but-surely increasingly usable proof assistants, which would be useful for a provable-not-corruptable (via normal software means) software kernel. Though... if one looks at the rate of advance in kernels over the past 30 years and then project out to the next 30, we get a distressingly high probability of it still being in C. Still, I cautiously optimistically (or pessimistically, depending) think that the hardware revolution that we are still only at the beginning of as we run out of Moore's Law is going to produce non-C languages that will eventually be irresistible to produce kernels in. There's going to be ever more constraints we want to maintain and it's going to get harder and harder to maintain them without some sort of language support beyond what C can supply.