The premise in the post is good but functional promoting posts are almost always silly. This one isn’t an exception.
You got this misconception that functional programming is about maintaining state. The people then answer to you that state is needed anyway. But that’s not the point because this maintaining state -viewpoint kind of misses the point because it’s too narrow.
Types encode the known behavior of the program. If we take the recipe example in this thing, your type might be:
⊸ 2 cups flour
⊸ Oven heated at 400F degrees
⊸ kitchen equipment
⊸ 60 minutes
⊸ (10 cupcakes ⊗ oven ⊗ kitchen equipment)
The proof would contain the recipe, the strategy you use to produce 10 cupcakes and not lose the oven and your other equipment. You use the logic-correspondence of the types to present the problem. For convenience I used linear types here because it’s a kitchen recipe. I assumed your tools don’t break when you use them.
Now consider how much easier it’s to navigate through a program where it’s explicit what we are expecting from it, and written such that the program cannot violate the expectations, at least not completely?
Of course this means you need pure and typed, and maybe even non-turing complete language, but I think functional as-it is just hype.
Hmmm. As someone with zero professional functional programming experience, I thought the post was pretty good at explaining why I might be interested in learning more about the paradigm.
To be honest, I am not sure I understand your comment–some of the terms are new to me :) .