5 ms·

The whole issue of the role of types is one of my current meditations. Python's duck typing is great for getting out of your way and getting on with your job.

The whole issue of the role of types is one of my current meditations. Python's duck typing is great for getting out of your way and getting on with your job. Usually. I'm just starting to work through some Julia toturials so that I can experiment with multiple dispatch. But I think the way to teach reasoning about types is to learn you some Haskell. I can't see doing a lot of production programming in Haskell today, but I think learning Haskell is a good mind-stretching exercize (just as learning Prolog was, back when Prolog mattered.)

nickpsecurity 10y ago
I agree Haskell will stretch my mind on the subject when I get around to learning it. It's exactly that reason that I've put it off for so long. ;) Far as industry, I'm not feeling as strong doubts as you looking at the quantity and diversity of this list: https://wiki.haskell.org/Haskell_in_industry https://wiki.haskell.org/Haskell_in_industry There's some real ass-kicking going on in industry with Haskell even if it's niche use and has obstacles/issues from that perspective.
- pjmlp 10y ago
  Do it, Haskell is great learning exercise. I never get to use it at work, but it helped improve my skills when using FP concepts in C++, JVM and .NET languages.
  - nickpsecurity 10y ago
    I might. My idea is to use either it or more pure ML/Ocaml to code the prototype up then convert each function into imperative C, Rust, or Ada. I figure a subset of Haskell should make that achievable. So, I can use all the tools like QuickCheck and QuickSpec for Haskell along with functional style to knock out many issues. Then, direct translation to imperative with no global issues, equivalence testing generated from Haskell tests, and static analysis to ensure local code is proper. That seL4 matched Haskell and C... along with open-sourcing a key tool (AutoCorres)... makes me think this is achievable. My method isn't formal proof but would be more accessible. What do you think?
    - pjmlp 10y ago
      You can already generate C from Haskell using jhc compiler: http://repetae.net/computer/jhc/ http://repetae.net/computer/jhc/ It doesn't support all the language features, though. Besides their standard one, GHC also has an additional LLVM and an older, now deprecated, C backends: https://downloads.haskell.org/~ghc/7.6.3/docs/html/users_guide/code-generators.html https://downloads.haskell.org/~ghc/7.6.3/docs/html/users_gui... The UHC also has a C backend, but not fully implemented, http://foswiki.cs.uu.nl/foswiki/Ehc/UhcUserDocumentation#A_6.6.1_61C_61:_GRIN_based_C_44_with_whole_program_analysis http://foswiki.cs.uu.nl/foswiki/Ehc/UhcUserDocumentation#A_6... Sounds a good idea, on the other hand have you ever used Frama-C? Never used it, but it seems being used in this kind of scenarios.
      - nickpsecurity 10y ago
        Thanks for links. So, here we go. re generating C. The key thing is whether it generates human-readable and -editable C. Most of those tools are used to just feed and piggyback on a C compiler. In my scheme, the Haskell is like the high-level, executable spec with C being equivalent. Such tools might be a start on my goal. I like that JHC has no garbage collector. That's promising for same reason Rust having no GC is. :) re Frama-C. Oh, yeah, that's good thinking as it's already been used for plenty C verification, even standard library. I was thinking of encoding Haskell specs in Frama-C somehow but not sure as I'm not formal methods specialist. Anyway, you might like where such techniques got their start for mainstream languages: http://apotheca.hpl.hp.com/ftp/pub/dec/SRC/research-reports/SRC-159.pdf http://apotheca.hpl.hp.com/ftp/pub/dec/SRC/research-reports/...
        the_why_of_y 10y ago
        GHC's C backend did not by any means generate anything a human would enjoy reading. It ran fast, though, on several platforms, which was the point.
        nickpsecurity 10y ago
        As I suspected. Thanks for the confirmation. I'm guessing human-readable output might have to be done at an earlier stage in the compiler to keep it close to original code. Or do it high-assurance style with each intermediate representation in C to let reader see what transformed code means.

nickpsecurity 10y ago

I agree Haskell will stretch my mind on the subject when I get around to learning it. It's exactly that reason that I've put it off for so long. ;) Far as industry, I'm not feeling as strong doubts as you looking at the quantity and diversity of this list: https://wiki.haskell.org/Haskell_in_industry https://wiki.haskell.org/Haskell_in_industry There's some real ass-kicking going on in industry with Haskell even if it's niche use and has obstacles/issues from that perspective.

pjmlp 10y ago
Do it, Haskell is great learning exercise. I never get to use it at work, but it helped improve my skills when using FP concepts in C++, JVM and .NET languages.
- nickpsecurity 10y ago
  I might. My idea is to use either it or more pure ML/Ocaml to code the prototype up then convert each function into imperative C, Rust, or Ada. I figure a subset of Haskell should make that achievable. So, I can use all the tools like QuickCheck and QuickSpec for Haskell along with functional style to knock out many issues. Then, direct translation to imperative with no global issues, equivalence testing generated from Haskell tests, and static analysis to ensure local code is proper. That seL4 matched Haskell and C... along with open-sourcing a key tool (AutoCorres)... makes me think this is achievable. My method isn't formal proof but would be more accessible. What do you think?
  - pjmlp 10y ago
    You can already generate C from Haskell using jhc compiler: http://repetae.net/computer/jhc/ http://repetae.net/computer/jhc/ It doesn't support all the language features, though. Besides their standard one, GHC also has an additional LLVM and an older, now deprecated, C backends: https://downloads.haskell.org/~ghc/7.6.3/docs/html/users_guide/code-generators.html https://downloads.haskell.org/~ghc/7.6.3/docs/html/users_gui... The UHC also has a C backend, but not fully implemented, http://foswiki.cs.uu.nl/foswiki/Ehc/UhcUserDocumentation#A_6.6.1_61C_61:_GRIN_based_C_44_with_whole_program_analysis http://foswiki.cs.uu.nl/foswiki/Ehc/UhcUserDocumentation#A_6... Sounds a good idea, on the other hand have you ever used Frama-C? Never used it, but it seems being used in this kind of scenarios.
    - nickpsecurity 10y ago
      Thanks for links. So, here we go. re generating C. The key thing is whether it generates human-readable and -editable C. Most of those tools are used to just feed and piggyback on a C compiler. In my scheme, the Haskell is like the high-level, executable spec with C being equivalent. Such tools might be a start on my goal. I like that JHC has no garbage collector. That's promising for same reason Rust having no GC is. :) re Frama-C. Oh, yeah, that's good thinking as it's already been used for plenty C verification, even standard library. I was thinking of encoding Haskell specs in Frama-C somehow but not sure as I'm not formal methods specialist. Anyway, you might like where such techniques got their start for mainstream languages: http://apotheca.hpl.hp.com/ftp/pub/dec/SRC/research-reports/SRC-159.pdf http://apotheca.hpl.hp.com/ftp/pub/dec/SRC/research-reports/...
      - the_why_of_y 10y ago
        GHC's C backend did not by any means generate anything a human would enjoy reading. It ran fast, though, on several platforms, which was the point.
        nickpsecurity 10y ago
        As I suspected. Thanks for the confirmation. I'm guessing human-readable output might have to be done at an earlier stage in the compiler to keep it close to original code. Or do it high-assurance style with each intermediate representation in C to let reader see what transformed code means.