It's talking about idealistic foundations. The idea that software being a theoretical language with a well defined domain and codomain can be written with zero bugs and zero testing to catch those bugs. Zero bug code is written utilizing the tools of math, such as axioms, theorems, and logic to derive zero bug code without the need to utilize engineering principles. (I'm exaggerating a bit with the word "zero", "nearly zero" is more accurate, but too wordy)

In practice we try to eliminate bugs in software engineering by doing testing as if software was some material with unknown properties. This method is easy to understand but ultimately has it's weaknesses as tests only prove a program works for a single test. This is the "foundation" most engineers are use to.

As I stated previously, the "foundation" these book refer to are an idealism involving proving an entire program to be bug free without running it or testing it. Hence this is the reason why it's so foreign to you. You're likely use to software from a testing perspective.

Vestiges of this "foundation" have leaked into the common practice of software engineering. It's called type checking. In type checking your computer uses a similar method to guarantee your program has zero type bugs. It doesn't run any type testing, it literally just proves that your program is type safe and correct.

Thank you for this comment, you shed some light on something I considered too opaque to dig into and made it clear why this would be useful.

> as if software was some material with unknown properties

That‘s a great way to put it!

Addition is something you learn in elementary school. Building the set of integers is taught in university.

Just because something is a foundation, doesn't mean it's easier to understand than the things build upon it.

I'm probably not the best person to say what I'm about to say.

In my university days, I took a graduate-level class called Software Foundations.

We used Haskell to learn and implement type systems and a few other things.

At the time I had no idea why it has "foundation" in the course title, because to me all of that was advanced stuff.

Eventually, I had my moment of enlightenment, and it all became clear to me. These where infact theoretical underpinnings of software.

Till then, I've only seen computation from the perspective of electricity->bits->circuits->...->assembly->the C language (and everything that comes above it).

Over there, the "foundation" was bits and electronics using which you can make logic gates, develop the arithmetic & logic unit (ALU) and control unit, and build everything on top.

On the other hand, with Lambda calculus, Church numerals etc I was approaching computation from the other direction — the mathematical perspective. It's also foundational, in that you can build up everything that you need — ALU and control unit — using Lambda calculus.

Indeed it was eerie the first time I added on paper two Church numerals using Lamba calculus and the correct result popped out. Even though I knew the theory was sound — and I know this is a dumb thing to say — it was still so cool to see it work in practice.

yeah it is a hard read. a relatively easier read is PLFA in Agda.