what about non-functional programming?

FP is just as irrelevant for most programmers as the math you already shoved aside

Hmm like the “new” JS Fetch api with `then` chaining? What about map, filter, reduce? Anonymous functions? List comprehensions? FP is everywhere. Pure FP code isn’t seen very often, as side effects are necessary for most classes of programs, but neither is pure OOP code, as not everything is dynamically dispatched, nor imperative code, as Objects or functions may more cleanly describe/convey something in code.

I shoved math aside because I think for most of the HN crowd it wouldn’t be a good use of their time to do what mainstream mathematics is about, like the “things such as Grothendieck schemes and perfectoid spaces” the article also references. FP is much more relevant because for any program for which a proof of correctness is worthwhile, you can always extract a functional core of that program (functional core, imperative shell). And that functional core will be easier to prove than if it were written in an imperative style.

FP and math are the same concept.

The semantics of math are equation based.

Everything in the math universal language is defined as an expression or formula.

All proofs are based on this concept.

To translate this into programming think about what programming is? Programming rather being a single line formula is a series of procedures.

  1. add 1
  2. add 3
  3. repeat.

That is essentially what functional programming is. Fitting your entire program onto one line OR fitting it into a math expression.

The reason why you see multiple lines in FP languages is because of aliasing.

  m = b + c
  y = x + m

  y = x + (b + c) 

So functional programming, one line programs, formulas and equations in math, and immutability are essentially ALL the same concept.

That is why lean is functional. Because it's math.