6 ms·

I tend not to use the phrase "systems programming" any more. "General purpose" is probably better (or my current favourite "Pac-man complete"). I should probabl

by edwinb 12y ago

I tend not to use the phrase "systems programming" any more. "General purpose" is probably better (or my current favourite "Pac-man complete"). I should probably edit the tutorial to that effect. We've done simple network protocols and packet formats (I had a student working on DNS for example) but not driver or kernel level things. That said, some people are experimenting with lower level things (thinking about making a minimal run time system with no garbage collection for example). It's not a primary goal, but it'll be interesting to see what comes of it.

bjz_ 12y ago
> I should probably edit the tutorial to that effect. Yes please do. Idris is a lovely language for bringing dependent types closer to the realm of production code, but giving people false hopes is a little cruel :)
- tel 12y ago
  Take a look at ATS then! My understanding from playing around with it is it is trying to be C with dependent types.
  - thinkpad20 12y ago
    ATS looks fascinating in concept, but what code examples I've seen, the syntax is terrible and it's ridiculously verbose. I'm sure you could write absolutely bulletproof code in it, but the productivity hit would render it almost unusable for large-scale projects. I might be off here, of course... but one of the lovely things about Haskell is that despite its reputation as a difficult language, once certain key concepts are tackled, it's relatively easy to program rapidly and create real world products (with a considerably higher assurance of correctness than most languages provide). ATS seems complex to a level that nearly guarantees its usage won't extend much beyond academia.
    - bjz_ 12y ago
      Indeed. I love the idea of ATS, but it seems like it would be a challenge to wrangle with. Whilst Rust isn't a flexible and powerful as ATS, it seems to be much easier to handle at the moment.
      - doublec 12y ago
        I think any language you're not familiar can seem like that - especially if it uses unfamiliar sigils or syntax. I feel similar about Rust for example as I'm not as experienced with it. But with ATS I can put programs together pretty quickly - all because I've learnt it.
        bjz_ 12y ago
        Thanks! Yeah, it's hard when you haven't used a language all that much to judge. I wish the sold themselves better though. The website is atrocious for folks wanting to get started with some code. :(
    - doublec 12y ago
      If you use the non-dependently typed parts of ATS it is no more verbose than most ML variants. If you use it without the GC then verbosity increased because you need to add calls to free memory. If you add proofs or dependent types then declaring those adds more. I've used it in moderately sized production programs and it's similar to using OCaml or other ML in terms of productivity. Once you're familiar with the language of course. If I paraphrase what you said about Haskell it's true for ATS too: "but one of the lovely things about ATS is that despite its reputation as a difficult language, once certain key concepts are tackled, it's relatively easy to program rapidly and create real world products (with a considerably higher assurance of correctness than most languages provide)." The key, like any language, is learning the concepts. I think people assume ATS is more difficult than it is is because much of the documentation and examples for it use a verbose style and heavy proofs. A post I wrote a while back attempts to gently introduce ATS dependent types and you can see that the non-dependently typed examples are very similar to any other ML language: http://bluishcoder.co.nz/2010/09/01/dependent-types-in-ats.html http://bluishcoder.co.nz/2010/09/01/dependent-types-in-ats.h...

by edwinb 12y ago

bjz_ 12y ago

> I should probably edit the tutorial to that effect. Yes please do. Idris is a lovely language for bringing dependent types closer to the realm of production code, but giving people false hopes is a little cruel :)

tel 12y ago
Take a look at ATS then! My understanding from playing around with it is it is trying to be C with dependent types.
- thinkpad20 12y ago
  ATS looks fascinating in concept, but what code examples I've seen, the syntax is terrible and it's ridiculously verbose. I'm sure you could write absolutely bulletproof code in it, but the productivity hit would render it almost unusable for large-scale projects. I might be off here, of course... but one of the lovely things about Haskell is that despite its reputation as a difficult language, once certain key concepts are tackled, it's relatively easy to program rapidly and create real world products (with a considerably higher assurance of correctness than most languages provide). ATS seems complex to a level that nearly guarantees its usage won't extend much beyond academia.
  - bjz_ 12y ago
    Indeed. I love the idea of ATS, but it seems like it would be a challenge to wrangle with. Whilst Rust isn't a flexible and powerful as ATS, it seems to be much easier to handle at the moment.
    - doublec 12y ago
      I think any language you're not familiar can seem like that - especially if it uses unfamiliar sigils or syntax. I feel similar about Rust for example as I'm not as experienced with it. But with ATS I can put programs together pretty quickly - all because I've learnt it.
      - bjz_ 12y ago
        Thanks! Yeah, it's hard when you haven't used a language all that much to judge. I wish the sold themselves better though. The website is atrocious for folks wanting to get started with some code. :(
  - doublec 12y ago
    If you use the non-dependently typed parts of ATS it is no more verbose than most ML variants. If you use it without the GC then verbosity increased because you need to add calls to free memory. If you add proofs or dependent types then declaring those adds more. I've used it in moderately sized production programs and it's similar to using OCaml or other ML in terms of productivity. Once you're familiar with the language of course. If I paraphrase what you said about Haskell it's true for ATS too: "but one of the lovely things about ATS is that despite its reputation as a difficult language, once certain key concepts are tackled, it's relatively easy to program rapidly and create real world products (with a considerably higher assurance of correctness than most languages provide)." The key, like any language, is learning the concepts. I think people assume ATS is more difficult than it is is because much of the documentation and examples for it use a verbose style and heavy proofs. A post I wrote a while back attempts to gently introduce ATS dependent types and you can see that the non-dependently typed examples are very similar to any other ML language: http://bluishcoder.co.nz/2010/09/01/dependent-types-in-ats.html http://bluishcoder.co.nz/2010/09/01/dependent-types-in-ats.h...