(The code examples here use idris https://www.idris-lang.org)
To augment testing with a finite number of inputs we write mathematical proofs that demonstrate their correctness on all possible inputs.
The programmer writes the proofs and the compiler checks the proofs as it builds the software.
New languages and tools are being developed. Agda, Coq and Idris for example that allow us to prove useful properties about programs in general-purpose programming languages.
To achieve this we need a richer type system than those found in normal industrial languages that we're familiar with.
We need types that we can talk about properties of a program. e.g for any list L, the reverse of the reverse of L is equal to L.
reverse : List a -> List a
reverse xs = ?reverse
reverseReverse : (xs : List a) -> reverse (reverse xs) = xs
reverseReverse xs = ?reverseReverse_rhsWe'll need to expore this type system a bit, in a language called idris. The syntax won't be too unfamiliar to Swift and Kotlin programmers because they've all been influenced by Haskell syntax.
We have the usual types Int, String etc. In Java / Swift we can have Types that depend on Types. e.g List<String>.
In Idris, types can also depend on values. And this is crucial to prove interesting things. Let's first look at equality type for Nat.
OnePlusOneIsTwo : Type
OnePlusOneIsTwo = 1+1 = 2This is a Type that represents the statement 1 + 1 = 2. Traditionally we think of this as a Boolean true or false. But we will think of this as a type which classifies the evidence that it's true. In the same way that Int classifies its members 1,2,3....
The equality type has constructor:
(=) : (x : Int) -> (y : Int) -> TypeWe'll write these types as 1 = 1, 1 = 2, 1 = 3, 2 = 2 etc.
A value of the type a = b is a proof of equality, so not all of the types have values.
There's no evidence for 1 = 2 means there's no value of this type. 1 = 1 has evidence so it has value. Idris
already knows that the type x = x has a value, it calls it Refl.
proofThatOnePlusOneIsTwo : OnePlusOneIsTwo
proofThatOnePlusOneIsTwo = ReflWhat if we try to prove that one plus one is three.
OnePlusOneIsThree : Type
OnePlusOneIsThree = 1+1 = 3
proofThatOnePlusOneIsThree : OnePlusOneIsThree
proofThatOnePlusOneIsThree = ReflProofs are related to execution. For our proof to be valid our compiler has to check that proofThatOnePlusOneIsTwo actually produces the value it claims. Idris can check for termination - but cannot always guarantee this due to the Halting problem.
proofThatOnePlusOneIsThree : OnePlusOneIsThree
proofThatOnePlusOneIsThree = proofThatOnePlusOneIsThreeThe compiler is happy with this but if we execute proofThatOnePlusOneIsThree we get an infinite loop. We need to check for termination to trust our proofs. Turing completeness is the enemy of reasoning.
Let's try something more challenging, proving statements about even and odd numbers.
Definition:
nis even if∃ k ∈ ℕsuch thatn = k + k
Write this in Idris as:
data Even : Nat -> Type where
MkEven : (half : Nat) -> (k = half + half) -> Even k
zeroIsEven : Even 0
zeroIsEven = MkEven 0 ReflThis pair of a value and a type that depends on the value is how we represent existental quantification. This is called a Σ-type.
Definition:
nis even if∃ k ∈ ℕsuch thatn = k + k + 1
Write this in Idris as:
data Odd : Nat -> Type where
MkOdd : (haf : Nat) -> (k = S (haf + haf)) -> Odd k
oneIsOdd : Odd 1
oneIsOdd = MkOdd 0 ReflTo provide evidence of the negation of a statement we have to provide evidence that the type associated with the statement has no values.
For example we know there's no evidence for 1 = 2 but there should be evidence
for not (1 = 2). We express negation in types as a type (1 = 2) -> Void where Void is the
empty type (i.e has no values).
We can provide evidence for this in idris as follows:
zeroIsNotOne : (Z = S Z) -> Void
zeroIsNotOne prf = absurd prfwhere absurd is a function provided by idris that converts a value of t -> a to a value of
a given that t is uninhabited (i.e has no values).
Idris already knows that some types are uninhabited (see doc: Uninhabited in the idris REPL for the full list).
In particular it knows that 0 = S n is uninhabited for any n. For other types like 1 = 2 we can
proceed by induction.
succIsInjective : S k = S j -> k = j
succIsInjective Refl = Refl
succNotEqual : (n : Nat) -> (n = S n) -> Void
succNotEqual Z prf = absurd prf
succNotEqual (S k) prf = let step = succNotEqual k in
step $ succIsInjective prfTo prove that zero is not odd we can use the same idea.
zeroIsNotOdd : Odd 0 -> Void
zeroIsNotOdd (MkOdd haf prf) = absurd prfIdris requires a bit more convinving that 1 is not Even.
oneIsNotEven : Even 1 -> Void
oneIsNotEven (MkEven Z prf) = absurd $ sym prf
oneIsNotEven (MkEven (S k) prf) = absurd $ succIsInjective (trans prf (sym $ plusSuccRightSucc (S k) k))Proof that one plus an even number is odd.
Produce evidence for Odd (S k) given evidence for Even k.
onePlusEvenIsOdd : Even k -> Odd (S k)
onePlusEvenIsOdd (MkEven half prf) = MkOdd half (cong prf)cong means congruence, expresses the fact that (a = b) => (f a = f b).
Proof that one plus an odd number is even.
Produce evidence for Even (S k) given evidence for Odd k.
onePlusOddIsEven : Odd k -> Even (S k)
onePlusOddIsEven (MkOdd haf prf) = MkEven (S haf) ?onePlusOddIsEven_rhs_2To prove this we need to prove the intermediate step:
haf + (S haf) = S (haf + haf)
Using plusSuccRightSucc haf haf:
S (haf haf) = haf + S haf
Using trans:
trans (k = S (haf + haf)) (S (haf + haf) = (haf + S (haf)) = (k = (haf + S (haf)))
onePlusOddIsEven : Odd k -> Even (S k)
onePlusOddIsEven (MkOdd haf prf) = MkEven (S haf) (cong (trans prf $ plusSuccRightSucc haf haf))Now we prove one final statement:
allEvenOrOdd : (k : Nat) -> Either (Even k) (Odd k)
allEvenOrOdd Z = Left zeroIsEven
allEvenOrOdd (S k) = case allEvenOrOdd k of
(Left l) => Right (onePlusEvenIsOdd l)
(Right r) => Left (onePlusOddIsEven r)This is an example of a function where the target type depends on the argument. Called a Π-type. Expresses universal quanitication.