Just this morning, when I was biking to work, I was thinking about this. For many decades I have felt that object-oriented has some flaws and that value oriented has more promises. You could consider transactions applied to databases as functions applied to a value. Some of the reasoning in the article, is about isolation. And the idea of pointers has some resemblems with. Whether two transaction influence each other (can be swapped) depend on whether the function that represent those transaction do commute.

But still, I think that the proposed solution is at the wrong level. I think it would be much better to talk about the specification versus the implementation level. Instead of saying this function works correctly when certain pre-conditions are met, you could also say that a function implements a function under for a certain value domain. The article, the function 'floorSqrt' could be viewed as a function, which implements the generic floor of square root function, for a certain value domain, namely positive 'int' values. (You wonder whether the input type was not of 'unsigned int'.) It is not even clear from the context, what is the maximum value of 'int'. That the result is always valid for the input values is clear.

I think that for the development of software engineering, it would be better to focus less on 'programming' languages and more on 'implementation' languages, languages that specify how a generic (often matchematical) problem, can be implemented in a programming language. Instead of developing yet another programming language.