3 ms·

The article seems to downplay the effect that space leaks can have on correctness / reliability. If 99.9% of code you write works, but every once in a while cod

by ummonk 4y ago

The article seems to downplay the effect that space leaks can have on correctness / reliability. If 99.9% of code you write works, but every once in a while code nondeterministically encounters space leaks, that's a bad thing for the reliability of the language as a whole. You can no longer rely on any program you write being guaranteed to execute to completion.

throwaway81523 4y ago
I would say in an exaggerated version of the Haskell mindset, the most important thing is to prevent the program from giving wrong answers. The archetypal Haskell program is a compiler, and having it generate wrong code that gets deployed on a space mission is disastrous. Having the compiler crash with a memory leak is merely an annoyance. You would not write realtime code in idiomatic Haskell, if you would write such code in Haskell at all.
- murdoze 4y ago
  Real-time code has high requirements for correctness and execution deadlines. Which means, w/o deterministic execution Haskell not suitable for a whole niche, where its safety properties are in a high demand. Which is a pity.
  - hexane360 4y ago
    Sure, but currently almost all of the most popular languages are also not suitable for that niche. If you exclude any garbage-collected language, you're basically left with Ada, C, C++, some of the "C/C++ successors" (Zig, D, Carbon, maybe Nim), and Rust.
  - throwaway81523 4y ago
    That's fine, those applications are why Ada was invented. Languages get pulled in too many directions when they try to be everything to everyone.
- ummonk 4y ago
  "OOM exception" is a wrong answer. If your code terminates on a space mission because lazy evaluation runs out of memory, it's disastrous.
  - throwaway81523 4y ago
    The code on the space mission wouldn't use Haskell or lazy evaluation. It would be written in something like Ada. In this picture, the Ada compiler would be written in Haskell. If the Ada compiler crashes with OOM, there is a disruption while you fix the leak, or run on a bigger machine as a stopgap. But if the output code crashes, that can ruin the space mission. So the main concern is that if the compiler doesn't crash, the generated code should be correct. Haskell's type system helps you write compilers that don't generate wrong code. As an even more extreme example, look at CompCert (compcert.inria.fr), which is a C compiler written in Coq. You can think of Coq as a dependently typed dialect of ML. For much of the backend, there are formal proofs that the output assembly code does the same thing as the input C code. The compiler is guaranteed to be free of a wide class of code generation bugs. But, AFAIK it is not guaranteed to be free of memory leaks or other crashes. Its reliability in that regard is just like any other software that has passed a reasonable amount of testing and has worked ok in production.
chriswarbo 4y ago
> If 99.9% of code you write works, but every once in a while code nondeterministically encounters space leaks, that's a bad thing for the reliability of the language as a whole. I don't know what you mean by "nondeterministic"? The behavious is occasionally hard to predict, but it's completely deterministic. Compare it to e.g. writing C in a certain style, relying on GCC to optimise it. Those optimisations might not apply for one chunk of code, so we end up with bad performance. Yet it's completely deterministic.
- bmitc 4y ago
  I think they probably more meant something like chaotic, in that small changes to your program can have big changes in the space leak space.
- ummonk 4y ago
  I should have said "undefined". What I meant was that the space the program will use isn't defined by the language itself and can't be known at compile time. It's dependent on implementation details of the compiler (GHC), and the particular input you feed to the program when executing it.
  - runeks 4y ago
    > What I meant was that the space the program will use isn't defined by the language itself and can't be known at compile time. You can know the space usage (in relation to input size) of some Haskell programs at compile-time — e.g. if you use a constant-memory streaming abstraction. I don’t know much about Rust, but I don’t think it guarantees known space usage of all possible programs at compile-time.
    - ummonk 4y ago
      Don't know if Rust has this ability, but SPARK (a subset of Ada for safety-critical code) does have the ability to guarantee known space usage, as well as guarantee that a program will terminate.

by ummonk 4y ago

throwaway81523 4y ago

I would say in an exaggerated version of the Haskell mindset, the most important thing is to prevent the program from giving wrong answers. The archetypal Haskell program is a compiler, and having it generate wrong code that gets deployed on a space mission is disastrous. Having the compiler crash with a memory leak is merely an annoyance. You would not write realtime code in idiomatic Haskell, if you would write such code in Haskell at all.

murdoze 4y ago
Real-time code has high requirements for correctness and execution deadlines. Which means, w/o deterministic execution Haskell not suitable for a whole niche, where its safety properties are in a high demand. Which is a pity.
- hexane360 4y ago
  Sure, but currently almost all of the most popular languages are also not suitable for that niche. If you exclude any garbage-collected language, you're basically left with Ada, C, C++, some of the "C/C++ successors" (Zig, D, Carbon, maybe Nim), and Rust.
- throwaway81523 4y ago
  That's fine, those applications are why Ada was invented. Languages get pulled in too many directions when they try to be everything to everyone.
ummonk 4y ago
"OOM exception" is a wrong answer. If your code terminates on a space mission because lazy evaluation runs out of memory, it's disastrous.
- throwaway81523 4y ago
  The code on the space mission wouldn't use Haskell or lazy evaluation. It would be written in something like Ada. In this picture, the Ada compiler would be written in Haskell. If the Ada compiler crashes with OOM, there is a disruption while you fix the leak, or run on a bigger machine as a stopgap. But if the output code crashes, that can ruin the space mission. So the main concern is that if the compiler doesn't crash, the generated code should be correct. Haskell's type system helps you write compilers that don't generate wrong code. As an even more extreme example, look at CompCert (compcert.inria.fr), which is a C compiler written in Coq. You can think of Coq as a dependently typed dialect of ML. For much of the backend, there are formal proofs that the output assembly code does the same thing as the input C code. The compiler is guaranteed to be free of a wide class of code generation bugs. But, AFAIK it is not guaranteed to be free of memory leaks or other crashes. Its reliability in that regard is just like any other software that has passed a reasonable amount of testing and has worked ok in production.

chriswarbo 4y ago

> If 99.9% of code you write works, but every once in a while code nondeterministically encounters space leaks, that's a bad thing for the reliability of the language as a whole. I don't know what you mean by "nondeterministic"? The behavious is occasionally hard to predict, but it's completely deterministic. Compare it to e.g. writing C in a certain style, relying on GCC to optimise it. Those optimisations might not apply for one chunk of code, so we end up with bad performance. Yet it's completely deterministic.

bmitc 4y ago
I think they probably more meant something like chaotic, in that small changes to your program can have big changes in the space leak space.
ummonk 4y ago
I should have said "undefined". What I meant was that the space the program will use isn't defined by the language itself and can't be known at compile time. It's dependent on implementation details of the compiler (GHC), and the particular input you feed to the program when executing it.
- runeks 4y ago
  > What I meant was that the space the program will use isn't defined by the language itself and can't be known at compile time. You can know the space usage (in relation to input size) of some Haskell programs at compile-time — e.g. if you use a constant-memory streaming abstraction. I don’t know much about Rust, but I don’t think it guarantees known space usage of all possible programs at compile-time.
  - ummonk 4y ago
    Don't know if Rust has this ability, but SPARK (a subset of Ada for safety-critical code) does have the ability to guarantee known space usage, as well as guarantee that a program will terminate.