4 ms·

> The main gate to functional languages participating in, say, the Linux kernel is NOT that they are "too slow" or that "laziness makes them too confusing". It'

> The main gate to functional languages participating in, say, the Linux kernel is NOT that they are "too slow" or that "laziness makes them too confusing". It's that the Linux kernel is written entirely around the unique weirdness and expectations of C, and only languages based on or descendant to C do well there. Sure, but the usual functional style has intrinsic issues that prevent it from being feasible for writing kernels in general. A kernel (especially a microkernel) spends most of its time managing state. You can use a functional language as a metalanguage for an imperative DSL (as the Atom DSL for constant-space programming uses Haskell), but you won't be writing code that looks remotely functional.

KirinDave 10y ago
> Sure, but the usual functional style has intrinsic issues that prevent it from being feasible for writing kernels in general. Not really? > A kernel (especially a microkernel) spends most of its time managing state. So does every computer program though. The idea that functional languages can't support mutation is a strangely persistent myth even in the face of multiple counter-examples AND 20 years of improvement via research and practical work. > but you won't be writing code that looks remotely functional. Many useful & powerful functional abstractions can be written to use constant space, even in Haskell.
- johncolanduoni 10y ago
  My point is not that functional languages can't support mutation, I'm well aware of the whole gamut from State to F-Star, Eff, and Idris. My point is that you're going to spend almost all of your time explicitly mutating things, using whatever functional language as a "very fine imperative language." Yes, you can embed those semantics inside functional semantics, and even use the functional language to add more static verification at the type level via things like F-Star's Hoare logic. But you're still mostly going to shoving bits in specific places based on the result of a shallow pure function applied to bits you yanked from a specific place. On top of that, you're not going to be able to abide the kind of allocations that functions in Haskell, OCaml, etc. can do with little provocation (and which are hard to avoid categorically), so you'll need to work within an especially restrictive DSL. Definitely no lambdas or partial application. So in the end you'll be in "Generic Stack-focused Pointer-pushing Procedural Imperative Language: The Monad". Where in this do you see any functional-ness, outside of the fact that you'll probably call your procedures functions? > Many useful & powerful functional abstractions can be written to use constant space, even in Haskell. Yes, but not to the degree that Atom's use cases require (where the program must allocate all memory ahead of time and therefore know a specific upper bound). This necessitates deviation from usual practices of any kind, including Haskell's.
  - KirinDave 10y ago
    > My point is not that functional languages can't support mutation, I'm well aware of the whole gamut from State to F-Star, Eff, and Idris. My point is that you're going to spend almost all of your time explicitly mutating things, using whatever functional language as a "very fine imperative language." The difference being that this "very fine imperative language" has much stronger type safety guarantees. Maybe we can stop having ring0 buffer overflows some day when C programmer pride is sufficiently assuaged. I doubt it though... My experience with the linux kernel community is that it is a limitless void of insecurity and infighting. > On top of that, you're not going to be able to abide the kind of allocations that functions in Haskell, OCaml, etc. can do with little provocation OCaml does much better here (in fact, really quite amazingly well here, on part with some of the greatest common lisp distribution compilers which were stunningly good at it). But yeah, Haskell has a very poor focus on the needs of the "industry" when said industry is focused around extremely tight optimizations. That said, I refuse to confuse a specific example of FP with a traditionally academic and research focus with the discipline as a whole. That's a dodge. > So in the end you'll be in "Generic Stack-focused Pointer-pushing Procedural Imperative Language: The Monad". Honest question: what's the problem with this if it offers additional safety and promotes the use of stateless functions? If it all compiles down to similar code, then it's fine. People act like monadic code is not functional, when it is in fact extremely functional code. That's what's funny about all this: imperative programming is expressible succinctly and easily in functional languages.
    - johncolanduoni 10y ago
      It's not a problem at all, it's exactly the direction I'd like to see things go as well. It's just that your code is still a stranger in a strange land in these cases. Your proofs will be full of the typical halmarks of functional programing, and for the stuff that is executed at runtime you'll definitely want some pattern matching, but there will be no closures or higher-order functions and limited opportunities for monads, functors, etc. Would you consider a C program transliterated into a representation of C inside a functional language and then annotated with proofs to be "functional"? My argument is what you get if you write a true kernel (no sitting on top of a runtime written in something else) is going to look a lot like that would.
- AnimalMuppet 10y ago
  A kernel spends most of it's time managing mutable state. Here's a table of processes. We want it to be an array, rather than a linked list, for efficiency reasons. When a new process is created, we don't want to copy the array, also for efficiency reasons. So we mutate the array. > So does every computer programmer though. Not really.
  - KirinDave 10y ago
    > A kernel spends most of it's time managing mutable state. Why do you think that FP doesn't have tools for this? Do you genuinely think that in 20+ years of research no one has thought of this? Have you investigated it? I don't know. If you think that things like ST aren't suitable please say why (other than the larger problems with monad transformers, of course).
    - AnimalMuppet 10y ago
      I know that FP has tools for that. But if the problem is primarily managing mutable state, isn't a tools that lets you directly see what you're doing a better fit? Are the FP tools as efficient as the direct, C-style approach? For an OS, that matters. Are the FP tools as easy to reason about correctly (especially in a section you're not familiar with)? For an OS that's worked on by thousands of people, that matters. In this context, what is "ST"? And, what are the larger problems with monad transformers?
      - KirinDave 10y ago
        What's most frustrating about these conversations is what I've noted in another thread: people feel really comfortable talking about what FP can and can't do without even acquainting themselves with 10+ year old techniques in the field. I'm sorry, I decline to continue this conversation further.
      - pjmlp 10y ago
        How do you think Xerox PARC, Genera and TI managed to write Lisp based OSes?
nickpsecurity 10y ago
Does COGENT look functional or imperative in programming style to you? Genuine question as I don't do FP. COGENT is latest in attempts at bringing functional, verified languages into system space. A team already redid the ext2 filesystem with it. https://ts.data61.csiro.au/projects/TS/cogent.pml https://ts.data61.csiro.au/projects/TS/cogent.pml
- johncolanduoni 10y ago
  COGENT takes pretty much precisely the approach I described below: it uses domain-specific structures in a functional language to encode verified imperative code. If you look at pretty much any code in the ext2 pilot (here[1] is as good as any) you'll notice that a lot of the functions called are things like destroy_Ext2DirEnt (which unless they named things poorly, takes a clear action), as well as a lot of passing around of memory addresses to functions that write them (e.g. deserialise_Ext2DirEnt2). It's not that they wrote the logic in a fundamentally different paradigm from C, it's that they take care to give their system the information it needs to both generate C code and most of the desired proofs simultaneously. The functional language is fufilling the role of metalanguage excellently, but little of that ends up in the generated code. The one functional thing that does is pattern matching, since the C equivalent (if statements and unions) are much harder to verify (and use). [1]: https://github.com/NICTA/cogent/blob/master/impl/ext2/cogent/src/dread.cogent https://github.com/NICTA/cogent/blob/master/impl/ext2/cogent...
  - nickpsecurity 10y ago
    Thanks for the insightful reply. I agree that code does look very imperative. Likely due to goal of C synthesis as you said.

KirinDave 10y ago

> Sure, but the usual functional style has intrinsic issues that prevent it from being feasible for writing kernels in general. Not really? > A kernel (especially a microkernel) spends most of its time managing state. So does every computer program though. The idea that functional languages can't support mutation is a strangely persistent myth even in the face of multiple counter-examples AND 20 years of improvement via research and practical work. > but you won't be writing code that looks remotely functional. Many useful & powerful functional abstractions can be written to use constant space, even in Haskell.

johncolanduoni 10y ago
My point is not that functional languages can't support mutation, I'm well aware of the whole gamut from State to F-Star, Eff, and Idris. My point is that you're going to spend almost all of your time explicitly mutating things, using whatever functional language as a "very fine imperative language." Yes, you can embed those semantics inside functional semantics, and even use the functional language to add more static verification at the type level via things like F-Star's Hoare logic. But you're still mostly going to shoving bits in specific places based on the result of a shallow pure function applied to bits you yanked from a specific place. On top of that, you're not going to be able to abide the kind of allocations that functions in Haskell, OCaml, etc. can do with little provocation (and which are hard to avoid categorically), so you'll need to work within an especially restrictive DSL. Definitely no lambdas or partial application. So in the end you'll be in "Generic Stack-focused Pointer-pushing Procedural Imperative Language: The Monad". Where in this do you see any functional-ness, outside of the fact that you'll probably call your procedures functions? > Many useful & powerful functional abstractions can be written to use constant space, even in Haskell. Yes, but not to the degree that Atom's use cases require (where the program must allocate all memory ahead of time and therefore know a specific upper bound). This necessitates deviation from usual practices of any kind, including Haskell's.
- KirinDave 10y ago
  > My point is not that functional languages can't support mutation, I'm well aware of the whole gamut from State to F-Star, Eff, and Idris. My point is that you're going to spend almost all of your time explicitly mutating things, using whatever functional language as a "very fine imperative language." The difference being that this "very fine imperative language" has much stronger type safety guarantees. Maybe we can stop having ring0 buffer overflows some day when C programmer pride is sufficiently assuaged. I doubt it though... My experience with the linux kernel community is that it is a limitless void of insecurity and infighting. > On top of that, you're not going to be able to abide the kind of allocations that functions in Haskell, OCaml, etc. can do with little provocation OCaml does much better here (in fact, really quite amazingly well here, on part with some of the greatest common lisp distribution compilers which were stunningly good at it). But yeah, Haskell has a very poor focus on the needs of the "industry" when said industry is focused around extremely tight optimizations. That said, I refuse to confuse a specific example of FP with a traditionally academic and research focus with the discipline as a whole. That's a dodge. > So in the end you'll be in "Generic Stack-focused Pointer-pushing Procedural Imperative Language: The Monad". Honest question: what's the problem with this if it offers additional safety and promotes the use of stateless functions? If it all compiles down to similar code, then it's fine. People act like monadic code is not functional, when it is in fact extremely functional code. That's what's funny about all this: imperative programming is expressible succinctly and easily in functional languages.
  - johncolanduoni 10y ago
    It's not a problem at all, it's exactly the direction I'd like to see things go as well. It's just that your code is still a stranger in a strange land in these cases. Your proofs will be full of the typical halmarks of functional programing, and for the stuff that is executed at runtime you'll definitely want some pattern matching, but there will be no closures or higher-order functions and limited opportunities for monads, functors, etc. Would you consider a C program transliterated into a representation of C inside a functional language and then annotated with proofs to be "functional"? My argument is what you get if you write a true kernel (no sitting on top of a runtime written in something else) is going to look a lot like that would.
AnimalMuppet 10y ago
A kernel spends most of it's time managing mutable state. Here's a table of processes. We want it to be an array, rather than a linked list, for efficiency reasons. When a new process is created, we don't want to copy the array, also for efficiency reasons. So we mutate the array. > So does every computer programmer though. Not really.
- KirinDave 10y ago
  > A kernel spends most of it's time managing mutable state. Why do you think that FP doesn't have tools for this? Do you genuinely think that in 20+ years of research no one has thought of this? Have you investigated it? I don't know. If you think that things like ST aren't suitable please say why (other than the larger problems with monad transformers, of course).
  - AnimalMuppet 10y ago
    I know that FP has tools for that. But if the problem is primarily managing mutable state, isn't a tools that lets you directly see what you're doing a better fit? Are the FP tools as efficient as the direct, C-style approach? For an OS, that matters. Are the FP tools as easy to reason about correctly (especially in a section you're not familiar with)? For an OS that's worked on by thousands of people, that matters. In this context, what is "ST"? And, what are the larger problems with monad transformers?
    - KirinDave 10y ago
      What's most frustrating about these conversations is what I've noted in another thread: people feel really comfortable talking about what FP can and can't do without even acquainting themselves with 10+ year old techniques in the field. I'm sorry, I decline to continue this conversation further.
    - pjmlp 10y ago
      How do you think Xerox PARC, Genera and TI managed to write Lisp based OSes?

nickpsecurity 10y ago

Does COGENT look functional or imperative in programming style to you? Genuine question as I don't do FP. COGENT is latest in attempts at bringing functional, verified languages into system space. A team already redid the ext2 filesystem with it. https://ts.data61.csiro.au/projects/TS/cogent.pml https://ts.data61.csiro.au/projects/TS/cogent.pml

johncolanduoni 10y ago
COGENT takes pretty much precisely the approach I described below: it uses domain-specific structures in a functional language to encode verified imperative code. If you look at pretty much any code in the ext2 pilot (here[1] is as good as any) you'll notice that a lot of the functions called are things like destroy_Ext2DirEnt (which unless they named things poorly, takes a clear action), as well as a lot of passing around of memory addresses to functions that write them (e.g. deserialise_Ext2DirEnt2). It's not that they wrote the logic in a fundamentally different paradigm from C, it's that they take care to give their system the information it needs to both generate C code and most of the desired proofs simultaneously. The functional language is fufilling the role of metalanguage excellently, but little of that ends up in the generated code. The one functional thing that does is pattern matching, since the C equivalent (if statements and unions) are much harder to verify (and use). [1]: https://github.com/NICTA/cogent/blob/master/impl/ext2/cogent/src/dread.cogent https://github.com/NICTA/cogent/blob/master/impl/ext2/cogent...
- nickpsecurity 10y ago
  Thanks for the insightful reply. I agree that code does look very imperative. Likely due to goal of C synthesis as you said.