@@ -616,24 +616,32 @@ Since Polonius is still unstable and will be so for the forseeable future, there
\section{Contracts and Refinement Types}\label{sec:contracts-refinements}
Every interface, be it a function, a library, or an \acs{HTTP} server, comes with a \emph{contract}: The interface expects data in a certain, well-defined form, and guarantees—given the input complies with this form—certain properties of the output. On the other hand, if the input is not well-formed, no guarantees on the output are made whatsoever. This principle is called “garbage in, garbage out”. If the interface exposes data, there are normally also some invariants that these data are supposed to conform to for the whole program run.
Every interface, be it a function, a library, or an \acs{HTTP} server, comes with a \emph{contract}: The interface expects data in a certain, well-defined form, and guarantees—given the input complies with this form—certain properties of the output. On the other hand, if the input is not well-formed, no guarantees on the output are made whatsoever. This principle is called “garbage in, garbage out”. If the interface exposes data, there are normally also some invariants that these data are supposed to conform to for the whole program.
Normally, these contracts are implicit and it is the burden of the author of an interface to carefully document them and the burden of the consumer of the interface to carefully follow them. This is not only a lot of work but also a large source for errors. This is why many programming languages offer some facilities to help users documenting and enforcing these contracts, the most notable being types. The input and output types of a function are part of its contract that can be extracted by a documentation tool and checked by the compiler.
Normally, these contracts are implicit and it is the burden of the author of an interface to carefully check and document them and the burden of the consumer of the interface to carefully follow them. This is not only a lot of work but also a large source for errors. Because of that, many programming languages offer some facilities to help users documenting and enforcing these contracts, the most notable being types. The input and output types of a function are part of its contract that can be extracted by a documentation tool and checked by the compiler.
Strong typing rejects some correct programs but also prevents many potential bugs and thus are used in many languages. The difficulties lie in how a type system should be designed. If a type system is too weak, it can’t find mistakes and is not very useful. On the other hand, strong type systems like the calculus of constructions\todo{citation} allow programmers to specify contracts down to the last detail and proof that an implementation follows this specification, but are very difficult to use and unwieldy.\footnote{A proof for the correctness of QuickSort in the language Coq spans several hundred lines: \url{https://gist.github.com/RyanGlScott/ff36cd6f6479b33becca83379a36ce49}}
Strong typing rejects some correct programs but also prevents many potential bugs and thus is used in many languages. The difficulties lie in how a type system should be designed: If a type system is too weak, it can’t find mistakes and is not very useful. On the other hand, strong type systems like the calculus of constructions\todo{citation} allow programmers to specify contracts down to the last detail and proof that an implementation follows this specification, but are very difficult to use and unwieldy.\footnote{A proof for the correctness of QuickSort in the language Coq spans several hundred lines: \url{https://gist.github.com/RyanGlScott/ff36cd6f6479b33becca83379a36ce49}}
In this section, we will focus on two related approaches of specifying contracts: Contract programming inserts explicit run-time checks into a program to ensure that it is never in an illegal state. Refinement types introduce compile-time checks. Finally, we will discuss hybrid typing, an approach to combine contract programming and refinement types.
In this section, we will focus on two related approaches of specifying contracts, that are very useful without being overly complex: Contract programming inserts explicit run-time checks into a program to ensure that it is never in an illegal state. Refinement types introduce compile-time checks. Finally, we will discuss hybrid typing, an approach to combine contract programming and refinement types.
\subsection{Contract Programming}
\todo[inline]{Example: Assertions}
Programming languages like Eiffel and D have native support for contract programming. There is also a library\footnote{Found under \url{https://gitlab.com/karroffel/contracts}} that brings design by contract to Rust. Contract programming enables three tools:
\item\emph{Preconditions} are checked at the beginning of some piece of code,
\item\emph{Postconditions} are checked after some piece of code has run, and
\item\emph{Invariants} must always hold for some piece of data.
\end{enumerate}
\todo[inline]{Example bank transfer: A bank account may never have a balance below lino of credit, a transfer precondition is that there is enough money in the first account, a postcondition is that the balancs are updated. Use Eiffel, D, or Rust/contracts?}
