The deep link equating math proofs and computer programs(quantamagazine.org)

    loginAdmin(name: &str, password: &str) -> Result<Admin, AuthenticationError>
    deleteDatabase(admin: Admin, dbConnection: &DbConnection, dbName: &str) -> Result<(), ConnectionError>

    let evilAdmin: Admin = unsafe { std::mem::transmute([0; size_of<Admin>()]) };
    deleteDatabase(evilAdmin, dbConnection, "important_data");

    anything : a
    anything = recurse 0
        where recurse i = recurse (i + 1)

    data Nat where
        0 : Nat
        S : Nat -> Nat  -- n + 1, "S"uccessor

    data Vec (n : Nat) a where
        Nil  : forall a, Vec 0 a
        Cons : forall n a, a -> Vec n a -> Vec (S n) a

    -- Instances of `IsTrue b` only exist if `b = True`
    data IsTrue (b : Boolean) where
        Trivial : IsTrue True

    -- Instances of `Every pred vec` only exist if every element in `vec` satisfies the predicate (so that `pred elem = True`)
    data Every (pred : a -> Boolean) (vec: Vec n a) where
        Every_nil : forall pred, Every pred Nil  -- Every item of an empty vector satisfies an arbitrary predicate
        -- Prepending an element which satisfies some predicate to a vector where every element satisfies the same predicate, produces a vector where every element satisfies the same predicate
        Every_cons : forall pred x xs, IsTrue (pred x) -> Every pred xs Every pred (Cons x xs)

    foosAreFoo : Every (\n -> n == "foo") (Cons "foo" (Cons "foo" (Cons "foo" Nil)))
    foosAreFoo = Every_cons Trivial (Every_cons Trivial (Every_cons Trivial Every_nil))

    head : Vec n a -> a
    head Nil = ???
    head (Cons x _) = x

    head : Vec (S n) a -> a
    head (Cons x _) = x
    

    data Var a = String

    -- Example IO monad which represents side-effects (stdin, stdout, and variables) through constructors
    data IO a where
        Pure      : a -> IO a
        ReadLine  : IO String
        PrintLine : String -> IO ()
        ReadVar   : Var a -> IO (Maybe a)
        WriteVar  : Var a -> Maybe a -> IO a
        (>>=)     : IO a -> (a -> b) -> IO b

    -- "Pure" program which reads first and last name and prints full name.
    -- The "interpreter" lazily computes the value of `main` and simultaneously evaluates `IO` actions to get their inner values:
    -- When it encounters (x >>= y) it computes `x`, evaluates `x` to get the inner value at runtime,
    -- then computes and evaluates `y`
    main : IO ()
    main =
        PrintLine "What is your first name?"  >>= \() ->
        ReadLine                              >>= \firstName ->
        PrintLine "What is your last name?"   >>= \() ->
        ReadLine                              >>= \lastName ->
        Pure (firstName ++ " " ++ lastName)   >>= \fullName ->
        PrintLine ("Hello " ++ fullName ++ "!")

    foo : Var Int
    foo = Var "Foo"

    -- Proving properties of programs is done with Hoare Logic.
    -- This is a lot more complicated and full of boilerplate...
    data Predicate where
        True  : Predicate
        (!==) : forall a, Var a -> a -> Predicate
        (/\)  : Predicate -> Predicate -> Predicate
    data HoareTriple (pre : Predicate) (stmt : IO ()) (post : Predicate) where
        Obvious  : forall pre stmt, HoareTriple pre stmt True
        Merge    : forall pre stmt post1 post2, HoareTriple pre stmt post1 -> HoareTriple pre stmt post2 -> HoareTriple pre stmt (post1 /\ post2)
        WeakenL  : forall pre1 pre2 stmt post, HoareTriple pre1 stmt post -> HoareTriple (pre1 /\ pre2) stmt post
        WeakenR  : forall pre1 pre2 stmt post, HoareTriple pre2 stmt post -> HoareTriple (pre1 /\ pre2) stmt post
        Specific : forall varN n, HoareTriple (varN !== n) (ReadVar varN >>= \nValue - WriteVar (varN + 1)) (varN !== (n + 1))
    example : HoareTriple
        (foo !== 4 /\ foo !== 5)                                -- Precondition
        (ReadVar foo >>= \fooValue -> WriteVar (fooValue + 1))  -- Statement
        (foo !== 5 /\ foo !== 6)                                -- Postcondition
    example = ...  -- Some combination of Merge, WeakenL, WeakenR, and Specific, but I've written enough

  Finally, a word or two about a wide-spread superstition, viz. that correctness proofs can only be given if you know exactly what your program has to do, that in real life it is often not completely known what the program has to do and that, therefore, in real life correctness proofs are impractical. The fallacy in this argument is to be found in the confusion between "exact" and "complete": although the program requirements may still be "incomplete", a certain number of broad characteristics will be "exactly" known. The abstract program can see to it that these broad specifications are exactly met, while more detailed aspects of the problem specification are catered for in the lower levels.