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.
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...
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.
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.
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.
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.
Is that a result of the specific language, rather than FP?
That is: One could think about building a procedural language that had... well, I'm not sure it could have Hindley-Milner types, because I'm not sure it could have higher-kinded types, but it could come close, couldn't it?
And from the other side: Does FP require very strong types? Or can it be done with something equivalent to C/C++'s type system? Or Python's?
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.
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).
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?
I'm sorry, I decline to continue this conversation further.
In many ways the early MIT Lisp Machine morphed into a Flavors Machine in the early 80s.
Remember, Lisp is a multi-paradigm language.
At least in Linux, the table of processes is implemented as a (doubly) linked list.
By the same token, whenever this conversation comes up a series of vague and poorly-formed criticisms come up saying, "You can't do low level things" without defining what on earth that means. Or, perhaps worse, conflating the idea that you must have Haskell in all its massive (and perhaps fairly: a bit bloated) confusion of ideas. People can and do write high performance code in functional style and with functional tools. People even do it with laziness as a core abstraction.
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.
It's difficult to treat the core question, "What are the disadvantages of functional programming" in the same way that it's difficult to answer, "What are the weaknesses of OO programming." Both use terms that encompass a very wide variety of approaches and decisions, but the way we evaluate them as bottom-up, on a case-by case language for each individual language.