How do we know that QuickSort does its job without errors? The answer lies in the proof of its correctness. In this article, we'll explore the challenges in automating the proof of QuickSort's correctness and the progress that has been made in this area.

QuickSort: A Brief Overview

QuickSort is a sorting algorithm that follows a "divide and conquer" strategy to sort a list of items. Here's how it works:

• Pivot Selection: The algorithm selects a pivot element from the list.
• Partitioning: The list is partitioned into two sublists: elements less than the pivot and elements greater than the pivot.
• Recursion: QuickSort is applied recursively to the two sublists.
• Combining Sublists: The sorted sublists are combined to produce a fully sorted list.

QuickSort's simplicity and efficiency make it a popular choice for sorting tasks, but ensuring its correctness is not as straightforward.

The Challenge of Proof Automation

Automating the proof of QuickSort's correctness is a non-trivial task, and there are several reasons for this:

1. Complex Algorithm Behavior: QuickSort's behavior is intricate and relies on comparisons and partitioning. Proving its correctness involves reasoning about the behavior of these comparisons and partitioning steps, which can become exceedingly complex for large datasets.
2. Infinite Input Space: QuickSort can theoretically be applied to an infinite number of inputs. Automating the proof for an infinite list is an immense challenge, leading to the need for focusing on specific cases. For instance, there is literature on correctness proofs of sorting arrays in Java rather than sorting any unbounded list of elements with some ordering. 
3. Complexity of Formalization: Most automation thus far actually relies on interactive theorem proving. That is to “automate” a proof, you need to formalize the algorithm and its correctness properties in a way that a proof assistant (e.g., Coq, Isabelle, Lean) can understand. This also requires proving each step manually even with machine assistance. This makes the formalization process time-consuming and tedious.
4. Complex Data Structures: QuickSort operates on complex data structures like arrays or lists. Proving the correctness of algorithms working with these data structures often involves reasoning about memory management and data manipulation, which complicates the automation process. This is particularly the case for proofs on real-world examples. In some cases, algorithms operate on real numbers or floating-point values, introducing additional complexities due to numerical precision.
5. Quantification and Induction: Many correctness proofs involve mathematical constructs like quantifiers (for all, there exists) and induction. Automating proofs that involve these constructs can be challenging because they require reasoning about arbitrary values and infinite cases. We will investigate this more closely in following blog articles. 
6. Human Insight: Humans often have intuitive insights that help them craft proofs effectively. Automation tools may lack this intuition and struggle with creative problem-solving. This also goes for superposition-based theorem provers such as Vampire that we base our work on. However, machines are also an opportunity. Since these proofs are mostly syntactic in nature, that is based on some rule applications we get a derivation that establishes a property, the automated provers sometimes find proofs that a human would not think of. 
7. The Halting Problem and Undecidability: QuickSort's behavior is influenced by the choice of pivot, making it difficult to prove that the algorithm always halts and produces a sorted result. The halting problem, a fundamental issue in computer science, states that it is undecidable to determine, in general, whether an arbitrary program will halt or not. This is essentially what makes our lives as logicians hard. 

Progress in Automated Proof

While automating the proof of QuickSort's correctness remains challenging, there has been notable progress in the field of formal verification and correctness proofs. Researchers and computer scientists are working to develop more robust and accessible tools to aid in the process. Some notable advancements include:

SMT (Satisfiability Modulo Theories) Solvers: These automated theorem proving tools can help with certain aspects of proof automation, particularly in proving the correctness of specific components of an algorithm.

Automated Formal Methods (often SMT-based): These are becoming more widely used in safety-critical systems. They involve rigorous specification and verification of software to ensure its correctness. While not fully automated, they significantly reduce the potential for errors.

Hybrid Approaches: Combining human insight and expertise with automated tools is often the most effective approach. Tools like interactive theorem provers allow human interaction to guide automated proofs.

Automating the proof of QuickSort's correctness is a complex challenge due to the algorithm's intricate behavior, infinite input space, and the limitations of automated tools. However, progress in formal verification and correctness proofs is continually being made, offering hope for more reliable automated verification in the future. Our aim is to prove such algorithms correct with the help of automated first-order theorem provers. We thus will investigate what it takes to make this happen.