2 ms·
I'm going to answer this question in the larger scope of "how does pure FP help us be confident that we are pushing correct code to production?" "Prove it" is
by whateveracct 10y ago
I'm going to answer this question in the larger scope of "how does pure FP help us be confident that we are pushing correct code to production?"
"Prove it" is our first line of defense. By always writing total functions, we can be confident that our services and jobs don't fail in uncontrolled ways. "Proving of theorems" is what you end up doing as you write total functions. NonEmptyList, ADTs, Options, Coproducts, These, singleton types, sized collections. All these things can provide powerful proof that is used to write total functions. The proof that various types provide makes it easier to write total functions as we can use Scala's powerful type system to greatly restrict which programs we even have to think about. And (thinking in reverse), forcing yourself to write pure, total programs ends up forcing you to prove various things about your program in order to achieve those properties.
So all in all, we perform the "proving of theorems" all the time. It just doesn't look or feel like it. But a large portion of CR discussion is about the types used in a program, which is in effect a discussion about which theorems we think we should prove before we push the code to production.