2

I have asked about the more nebulous 'system' and functions in general, but to explain my question let me just consider a pure function.

I think of pure functions as lemma/theorems/what have you. Given a function f and some conditions (inputs with some constraints), f applied to the conditions has some properties (e.g. is of a certain type).

An argument I often hear in favour of static typing is that they by way of some program which reads the source (e.g. a compiler) can provide a proof that certain properties hold for a function (e.g. the return is of a certain type). Unfortunately type systems in programming languages aren't practically capable of expressing all the constraints and all the properties the return of the function has, for instance the property that the return is a prime number.

On the other hand, if we are happy to just write informal proofs (in the relatively rigorous sense of the proofs presented in most mathematical papers) then we can provide proofs of whatever we like.

For a simple example where it is clearly practical, consider a large comment accompanying an implementation of a sieve of Eratosthenes, it can precisely describe the required inputs and the output, and argue that it does produce this, to be verified by other programmers.

I would like to know established approaches to this, drawbacks, and reasons why I have not seen this in practice?

I appreciate that such an approach would necessitate not changing the properties of a function once it has been established, but this is something I am happy to concede as it ties in with my view that a function is a theorem, once a theorem is in use and other theorems use it, you can't go changing its statement!

Edit -

There has been some confusion over the term 'informal proof' which I am to blame for, for the purpose of clarity, FilipMilovanović has a comment which is a good summary.

So, an informal proof in maths is really an informal statement that doesn't go into all details, but from which, in principle, a formal proof can be produced (extrapolated) I.e. there should always be a path to a formal proof. (So in that sense the distinction is superficial.) But this doesn't imply that the language features and type system are expressive enough to let you express the constituent statements of the proof in a way that can be checked by the compiler (which was not built as a general purpose theorem prover).

11
  • 1
    @FilipMilovanović They are usually referred to as formal proofs (maybe, I don't know) by non mathematicians, by mathematicians they are referred to as informal, they are informal in various senses, for instance there is no hope for a computer to verify them. Had I known this definition was going to be so contentious I would have been clearer and I am very sorry I didn't do so as it has somewhat derailed things. I am a mathematician, not a programmer, I didn't appreciate the term was understood this way by others. Oct 3, 2020 at 21:33
  • 1
    I'm pretty sure you got it backwards - mathematicians don't care if things are computable, they care if they can prove (within the formal mathematical framework they are using) if one thing logically follows from another. I could be wrong, but it doesn't really matter, as long as we understand what you mean. Oct 3, 2020 at 21:37
  • 1
    Oh, I see what happened. So, an informal proof in maths is really an informal statement that doesn't go into all details, but from which, in principle, a formal proof can be produced (extrapolated) I.e. there should always be a path to a formal proof. (So in that sense the distinction is superficial.) But this doesn't imply that the language features and type system are expressive enough to let you express the constituent statements of the proof in a way that can be checked by the compiler (which was not built as a general purpose theorem prover). Oct 3, 2020 at 21:51
  • 1
    Basically, if it helps others, the way I understood your question is: beyond the guarantees we can get from a compiler, are mathematical proofs used in practice to justify an implementation of a function (or a system), and if so, in what kinds of scenarios/domains (e.g. cryptography comes to mind), how are they documented, what are some of the practices surrounding their use, etc. Oct 3, 2020 at 22:07
  • 1
    Some of the topics are software formal methods, semantics of programming languages, program specification & program verification. There's a large literature including textbooks. You could start with Dave Parnas's work on formal specification & programming in software engineering.
    – philipxy
    Oct 4, 2020 at 3:16

1 Answer 1

7

I think of pure functions as lemma/theorems/what have you. Given a function f and some conditions (inputs with some constraints), f applied to the conditions has some properties (e.g. is of a certain type).

This is slightly incorrect.

What is correct is that there is a very deep connection between programming languages and logic, types and theorems, programs and proofs. Philipp Wadler has jokingly said that you can spot a good abstraction by the hyphen, because so many important results in programming language theory have double-barreled names, since they were independently discovered and proven twice, once in programming language theory, and one in logic.

Examples include the Curry-Howard Isomorphism (or the more general Curry-Howard-Lambek Correspondence which adds Category Theory to the mix), the Girard-Reynolds Isomorphism, the Damas-Hindley-Milner Type System, or the introduction of Type Classes by Wadler-Blott.

Under the Curry-Howard Isomorphism, there is a correspondence between types and propositions as well as programs and formulae. So, if we go back to your statement:

I think of pure functions as lemma/theorems/what have you.

We can be more precise and say

  • The return type of the function corresponds to a proposition.
  • The input parameter types of the function correspond to hypotheses.
  • The function corresponds to a formula that proves the proposition given the hypotheses.

This correspondence has been proven for several typed calculi and systems of logic, and we now accept a generalized correspondence that every type system induces a system of logic, and every system of logic induces a type system. It's just that many of them are not very useful, e.g. Java's type system induces a system of logic that is inconsistent and most systems of logic induce type systems that are unsuitable for programming languages.

An argument I often hear in favour of static typing is that they by way of some program which reads the source (e.g. a compiler) can provide a proof that certain properties hold for a function (e.g. the return is of a certain type).

That is indeed true. By way of the Generalized Curry-Howard Isomorphism, a type checker is a proof checker.

Unfortunately type systems in programming languages aren't practically capable of expressing all the constraints and all the properties the return of the function has, for instance the property that the return is a prime number.

As hinted at above, that depends on the type system and the system of logic it induces. For example, in dependently-typed programming languages such as Coq, Isabelle, Epigram, Agda, Guru, or the hip new kid on the block, Idris, it is possible to write something like this as a type: "For all types T, the function sort takes a list of Ts and returns a sorted list of Ts, such that the length of the sorted list is equal to the length of the original list, every element that is present in the sorted list is also present in the original list, every element that is present in the original list is also present in the sorted list, and for every consecutive pair of elements a and b of the sorted list, a ≤ b holds."

On the other hand, if we are happy to just write informal proofs (in the relatively rigorous sense of the proofs presented in most mathematical papers) then we can provide proofs of whatever we like.

For a simple example where it is clearly practical, consider a large comment accompanying an implementation of a sieve of Eratosthenes, it can precisely describe the required inputs and the output, and argue that it does produce this, to be verified by other programmers.

This can indeed be done, and there are formalizations for doing precisely this. For example, most programmers will probably have learned Floyd-Hoare Logic and Predicate Transformer Semantics in university.

The two systems I learned in university are both based on pre- and postconditions (as well as loop variants and invariants) and differ in the direction they are working in.

One system starts with the desired result of the program, i.e. the postcondition that you want to achieve, then for each statement you prove the weakest precondition, take this precondition as the postcondition of the preceding statement, and repeat until you arrive at the start of the program, and then you can check whether the precondition of the program covers all intended use cases. Imagine a program that computes the square root of a number (how exciting!) and you show that the weakest precondition of the whole program is that the input must be the square of an integer, but you actually want to compute the square root of an arbitrary non-negative floating point number. Then you have shown that the program does not do what you want to do. If, OTOH, the weakest precondition you can prove is that the input can be any floating point number, even negative, then you have proven that your program works not only for your use case, but even more use cases.

Or, you can work in the opposite direction, you start with your use case as a precondition (n ∈ ℝ+), prove the strongest postcondition of the first statement, take that to be the precondition of the next statement, and so on, until hopefully you arrive at the end at the postcondition that result × result = n.

I would like to know established approaches to this, […]

The general field you are talking about is called Formal Methods. It encompasses more or less anything that is related to applying mathematical rigor to Software Engineering.

One established Software Engineering Methodology (for various values of "established", i.e. in this case, I doubt anyone has every heard of it, but there have been articles written about it) that incorporates proofs into the Software Development Lifecycle is Clean Room Software Engineering.

Cleanroom is based on the following ideas:

  • Incremental Refinement: You start with a simple and small system, and then incrementally extend it in simple and small steps. This is true of practically all modern Software Engineering Methodologies, and in fact appears in Engineering in general even outside of Software (compare e.g. the difference in approaches between the development of the NASA Space Launch System and SpaceX's Starship/Superheavy).
  • Formal Verification: Software Engineers formally verify that the program meets the specification.
  • Statistically sound testing: Comprehensive testing using statistically sound methods, essentially applying the Scientific Method to testing.
  • Progress Testing: Not only do we apply testing to the program to check whether it is reliable in practice, but we also apply testing to the incremental process to check that we are actually making progress, i.e. for each increment we define a goal and then we verify that we have met that goal.

I would like to know […] drawbacks, and reasons why I have not seen this in practice?

The main reason why this is almost never done, is the amount of effort required. For example, Linux was written by Linus Torvalds alone, in his spare time, in a couple of weeks, while at the same time he was learning how to write an Operating System and learning how to program an i386 computer. seL4, a microkernel much simpler than Linux took an entire team of experienced Operating System developers, Computer Scientists, and mathematicians, 3 years just to produce the first proof, and 8 years in total, until the full source code and proofs were published.

And the first proofs actually explicitly excluded some critical parts such as the memory allocator and garbage collector. Also, while they proved that their implementation matched the specification, you still have the problem that you have no idea what the compiler does with your code. Now, eventually, they added memory allocation and garbage collection to the specification and proved their implementation correct, and later they also proved correctness of a C compiler with respect to (a formalized subset of) the C language specification, so they could actually successfully argue that the binary code they produce is correct with respect to the specification.

Oh, but that leaves the CPU! And in fact, they even later also proved a simple CPU correct with respect to its specification and proved that their C compiler produces correct code with respect to the CPU specification.

But all of this took a long time, cost a lot of money, and is still not really applicable for the "real world", since the simple CPU they proved correct is not used by anybody and in fact doesn't even exist in silicon, only in hardware description language. (Which BTW then poses the problem of also having to prove the correctness of the HDL compiler …)

The seL4 project is actually one of the most efficient projects employing formal methods with a cost of only ~400 $SLOC compared to the more typical 1000+ $SLOC, but that is still significantly higher than typical software development costs. In comparison, the FBI Virtual Case File (Project Trilogy), widely considered one of the most expensive and most embarrassing project failures in the history of Software Engineering cost 240 $SLOC. So, even the cheapest, most efficient formally verified software project in history is still almost twice as expensive as one of the worst failures of traditional approaches.

However, the cost and the long development times are actually not even the real problem. The real problem is that a proof proves exactly what it proves. In other words, proving a program correct with respect to a specification does exactly that: it proves that the program does what the specification says it must do.

However, the biggest problem we have in Software Engineering is not necessarily that programs don't match their specification but rather that specifications don't match user expectations. I can have the most beautiful, most elegant, most rigorous proof that my program indeed does "B", and it won't help one bit if it turns out that I misunderstood the user to say "A" but incorrectly formalized this statement to "B" when the user actually said "C" but wanted to say "D", and indeed meant to say "E" and discovered after playing around with the system that what they really want is "F" but what they actually need is "G" but they can't afford it so they will be content with subset "H".

Users simply can't write formal specifications, and even if they could, they wouldn't know what to write because they don't actually know what they want, and even if they did, what they want is often not what they need, and even if it were, their needs may change even before the project is finished.

The best way we know how to solve this problem is to rapidly prototype and rapidly iterate. We try to give the user an incomplete, simplified subset of the system as early as possible, so that they can start using it and discover whether what we built for them is actually what they want (and we can observe them and see whether what we built for them is actually what they need, which unfortunately is not necessarily the same thing.) And we repeat this as often and as early as possible. Formal Methods are unfortunately not conducive to this kind of rapid iteration.

In a lot of Software Engineering, time-to-market is the most important thing. It doesn't matter that your smart phone is proven correct if you can't sell any phones because the market has already been divided amongst your competitors who beat you to the release by compromising on quality. Similarly, price is important: it would be perfectly possible to have a smart phone that is proven correct, but who would pay 10000 $ for the equivalent of an entry-level phone from 5 years ago?

It doesn't matter if your software matches the specification you wrote down six months ago if the circumstances change every three months.

Formal Methods are used, but only in limited niches where Failure is not an option, cost and development time is not an object, and specifications are clear. Examples are medical devices or flight computer software. Even in banking, it is typically considered to be more cost-effective to forego Formal Methods and instead insure against the risk of losing your customers' money.

2
  • 1
    Excellent, just what I was looking for. I think the best thing for me to do now is read into seL4 that ought to be a fascinating case study Oct 4, 2020 at 8:51
  • To be fair, Linus is just responsible for the kernel of Linux. Oct 4, 2020 at 14:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.