The Power of 10: Rules for Developing Safety-Critical Code [pdf]

If you're the programmer who has to provably meet hard real time constraints, the difference matters quite a bit.

> You can do this even with libc malloc in a standards compliant way

This is what I do in nontrivial embedded projects. It makes things easier and less error-prone to replace malloc()/free()/etc implementations directly with ones that behave as needed. And then you don't have the standard implementations sitting around waiting for a new dev to accidentally use them.

Yep, it's a bit terrifying to contemplate. If you're ever unfortunate enough to do safety critical systems, you'll have to remember that you have to protect against this not only at the software level with formal methods, but also at the hardware level to ensure that e.g. a bit flip in the CPU registers or the instruction sequence as it travels from memory also doesn't violate your safety model.

> I'm not deep into more advanced flavors of functional programming, but I thought total functions are defined as terminating in finite time for all inputs.

The main paper that lays this out is "Total Functional Programming" (https://www.jucs.org/jucs_10_7/total_functional_programming/...).

But to briefly summarize:

I was playing a bit fast and loose with wording since most notions of total functions are built on top of FP languages as you point out and therefore ultimately on the lambda calculus where we don't have a native notion of a loop.

Instead of loops in FP languages we have lists (and folds on the list or an unfold to generate the list) and other data structures that reify the notion of iteration.

Hence what I was really saying is that a total function can also generate an infinite data structure, which is only roughly like saying an infinite loop.

Totality is usually formally defined in terms of data and codata (or equivalently recursion and corecursion). The co- prefix may sound a bit scary, but an informal way of thinking about it is that data is always finite and codata can be infinite. The canonical example is that a list is an example of data and an infinite, lazy stream is an example of codata.

This seems like a lot of ceremony for no real good reason if you consider an "infinite" data structure as simply a finite data structure that can store functions that happens to have additional computation in it hidden behind some closure. And indeed you are still correct that an informal and usually sufficiently useful definition of totality for a function is that it terminates in finite time for all inputs (after all even if you generate an "infinite" data structure you still terminate in finite time and just hide the additional computation within a finite data structure).

It's still nice to have the data vs codata distinction though.

Practically speaking bringing in the notion of codata gives us a nice little heuristic for checking termination when creating an infinite data structure. Only types marked as codata are allowed to have infinite descent and when returning them from a function we have to always follow a certain syntactic pattern known as guarded recursion. Otherwise if we didn't have the notion of codata, a naive termination checker would have a hard time with checking termination of a function that recurses on itself, but only behind a lambda.

E.g.

  // Pseudo-code

  data class Stream(head: Int, rest: () => Stream)

  // generateIncrementingStream(0) generates the infinite stream 0, 1, 2, ...
  generateIncrementingStream(start: Int): Int = {
    Stream(start,  () => generateIncrementingStream(start + 1))

    // This appears to a naive termination checker to never terminate
    // You could try to simply check if the recursive call is inside a function
    // but then you run into other issues if e.g. the entire function is called 
    // again and it becomes very thorny very quickly
    // e.g. Stream(start, {(() => generateIncrementingStream(start + 1))(); () => generateIncrementingStream(start + 1)}
    // never terminates even though all calls to generateIncrementingStream are 
    // contained behind lambdas. You might have to start doing some annoying 
    // symbolic computation.

  }

vs

  // Note that the recursive call to Stream in rest is no longer behind a lambda
  // Under the hood this might be implemented with lambdas
  codata class Stream(head: Int, rest: Stream)

  def generateIncrementingStream(start: Int): Stream = {
    // Much easier heuristic: all recursive calls must be inside a codata
    // constructor, i.e. "guarded" by a constructor call hence "guarded recursion"
    Stream(start, generateIncrementingStream(start + 1))
  }

The general idea here is that a function that generates codata is productive and hence total if it generates a finite amount of the potentially infinite codata structure before its next recursive call. A nice heuristic that captures most useful cases is guarded recursion (of course because of the halting problem this is only a heuristic).

The usual heuristic is that for functions that generate data, you must have structural recursion, i.e. every recursive call must be on a piece of data "smaller" than the original input. On the other hand if you generate codata, you must have guarded recursion, i.e. every recursive call must be guarded behind a codata constructor.

This resolves some things quite nicely. E.g. if have a recursive function that accepts a codata `Stream` and wants to return some data, e.g. a finite `List`, then we must have some other argument that gets smaller every function call. E.g.

  // Taking in infinite codata and producing finite data
  def take(stream: Stream, n: NaturalNum): List[Int] = {
    n match {
      // This passes totality checking because m is "smaller" than n, which here
      // means we had to strip away one level of NaturalNum constructors
      // hence 
      Successor(m) => Cons(stream.head, take(stream.rest, m))
      Zero => EmptyList
    }
  }

  
  def streamIdentity(stream: Stream): Stream = {
    // Since we're producing codata, we check for guarded recursion
    // Passes totality checker because streamIdentity is guarded behind Stream
    Stream(stream.head, streamIdentity(stream.rest))
  }

  def listIdentity<A>(list: List[A]): List[A] = {
    list match {
      case EmptyList => EmptyList
      // Since we're producing data, we check for structural recursion
      // Passes totality checker because the recursive call is on a smaller piece of data
      case Cons(x, rest) => Cons(x, listIdentity(rest))
    }
  }

  // Can't blindly produce finite data from an infinite piece of codata!
  def nontotalStreamToList(stream: Stream): List[Int] = {
    // Looking for structural recursion
    // Does not pass totality checker because stream.rest is not considered to be smaller than stream since Stream is codata
    Cons(stream.head, nontotalStreamToList(stream.rest))
  }

  // Can definitely produce infinite codata from finite data though
  def padOutListWithInfiniteZeroes(initialSegment: List[Int]): Stream = {
    initialSegment match {
      case Cons(x, rest) => Stream x (padOutListWithInfiniteZeroes(rest))
      case EmptyList => Stream 0 (padOutListWithInfiniteZeroes(initialSegment))
    }
  }

Bringing in the notion of codata also gives us some theoretical nicety. How do you express totality for a program that must run forever, e.g. a server? You say that the IO type a la Haskell is codata and that's that! Then you know that `main` having the `IO` type means that it can potentially run forever, but it will always generate a finite amount of stuff on every codata "iteration" and therefore is productive and is not just spinning its wheels in a pointless infinite loop that does nothing.

Clang provides the "musttail" attribute for C and C++:

https://clang.llvm.org/docs/AttributeReference.html#musttail

Bounding the complexity is desirable for a system that should never fail due to software errors.

You can easily have bounded loops and superexponential runtime.

When everything is finite and memory is always limited, what are you meaningfully saying about the possible behaviors of software here?

I have worked on a safety critical system and can't recall a part that needed Turing completeness.

The automotive industry is weird like that. They started doing things a way, got stuck in a groove and now if you push back against it they look at you like you killed their dog.

I should really find a different field, for my mental well being.

It's doable sometimes when there's a tailoring framework. Here's a publicly available example [1]. Though I admit that it's usually easier to do in the US than in the European Union, so your experience may vary.

[1] https://www.nasa.gov/seh/3-11_tailoring_and_customization