Ask HN: How do you verify an algorithm’s correctness

[lazyfolder]

The most intuitive way I know to disprove an algorithm is by finding a counter example. But for complex algorithms it can be hard to find a counter example.

Do you have any practical advice? Should I learn formal proofs?

[armchairhacker]

First you have to define "correctness". Often this is "the result satisfies some predicate (which is another computation)"

Then you can use formal methods. For example in Coq you may do something like:

    (* Some algorithm which takes one number as an input, of course you can have it take any arguments *)
    Definition the_algorithm (x : nat) : nat :=
        ...
    .

    (* Another algorothm which checks that the output is expected *)
    (* You can use 'Inductive' or 'Defintion' to define this, each has its benefits and drawbacks *)
    (* 'Inductive' is a GADT where instances have valid inputs / outputs *)
    (* You can also write the_algorithm as a 'Definition' with some fuel parameter and return an 'option nat' if your function can't be proven terminating, etc. *)
    Inductive check_the_algorithm : nat -> nat -> Prop :=
    | BaseCase : check_the_algorithm 0 0
    | AnotherCase : forall i o, check_the_algorithm i o -> check_the_algorithm i (i * 2)
    | ...
    .

    (* This is the key part, which proves the algorithm is "correct" *)
    Theorem the_algorithm_is_correct : forall n, check_the_algorithm n (the_algorithm n).
    Proof.
        ... (* Here you will prove it using tactics *)
    Qed.

[mepian]

I recommend looking into ACL2, an industrial-strength theorem prover that's used for software and hardware verification by companies like Arm, AMD, and Intel: https://www.cs.utexas.edu/users/moore/acl2/

[brad0]

TLA+ and the like could help here. You model the system, and run a simulation to see if it hits a failure state.