<p>Here is a natural problem from graph theory where the proof and the algorithm are closely intertwined. In my view, one can discover this algorithm only via thinking about the proof and the algorithm "in parallel." The task is this:</p>

<p><strong>Input:</strong> An undirected graph.</p>

<p><strong>Task:</strong> Find a subgraph with maximum edge-connectivity.</p>

<p><strong><em>Note:</em></strong> What makes the task non-trivial is that a subgraph can have larger edge-connectivity than the whole graph. Since there are exponentially many subgraphs, it would take exponential time to check all of them to find the most connected one, even though we can compute the edge-connectivity of any graph in polynomial time.</p>

<p>Below is a part of a lecture note about solving this problem. It shows that the task can be solved in polynomial time, using a subroutine that finds a minimum cut (which is well know to be doable in polynomial time). For short, edge-connectivity is just called connectivity, and is denoted by <span class="math-container">$\lambda(G)$</span>.</p>

<p><a href="https://i.sstatic.net/azaAv.png" rel="noreferrer"><img src="https://i.sstatic.net/azaAv.png" alt="Finding a subgraph with maximum edge connectivity"></a></p>

CC BY-SA 4.0
2020-01-06T08:48:05.997Z
This is a nice example problem! I might see if I can use it when we do divide & conquer (we typically do that before mincut, but I can give them mincut as an oracle and it will also be nice foreshadowing). In terms of the proof though, if you just want polynomial time, isn't it trivial that mincut is called at most O(m) times (m=# edges), since each time you call it you remove at least one edge?
Joshua Grochow
CC BY-SA 4.0
2020-01-06T22:57:04.233Z
@JoshuaGrochow Yes, you are perfectly right! Even if the graph has exponentially many edges (it is possible, due to parallel edges, which were not excluded), your argument still carries over, since each min cut call removes at least one full bundle of edges (=all edges between two nodes), and there are at most $n(n-1)/2$ such bundles. However, the $f(n)\leq n-1$ bound is tighter. In fact, it can hold with equality, as shown by the example of an induced path.
Andras Farago
CC BY-SA 4.0
2020-01-02T18:49:56.723Z
2020-01-02T18:49:56.723Z
Andras Farago
<p>A practical answer: In my career I encountered a few scenarios, some with my direct involvement, where I had to prove that my algorithm performs just as good as the currently best known possible. There are many examples where such knowledge can have a direct effect on one's career... In my experience, making a good claim at a design review meeting or to your direct boss can sometimes be more important than actual implementation.
Some examples: 
The first "trivial" example was at the very beginning of my career. 
I was the only "engineer" in the company. 
The internet was only at it's beginning and they wrote code for median finding by first sorting the numbers and then take the center element.
I actually had to explain why the linear time algorithm actually works in linear time...
The second one involved 2D correlation for motion detection. 
The idea is too long to explain here, but I had to explain (prove) why the specific conditions of the problem makes it possible for my algorithm to run faster than the obvious one.</p>

CC BY-SA 4.0
2020-01-02T22:31:15.330Z
2020-01-03T03:14:48.467Z
2020-01-03T03:14:48.467Z
Avi Tal
<p>I see several advantages of mastering the proof of correctness and complexity of an algorithm. I list them below and illustrate with a concrete example. I tried to stay in the domain of classical textbook algorithms. </p>

<h1>Understanding why the algorithm works</h1>

<p>Certainly the most obvious reason of having proofs. Many algorithms exploit some structure in the problem in a non obvious way. Without proving their correction, there is no way to really understand why it works. Without understanding this, there is no way of really implementing it. </p>

<p>One example of such algorithm is the <strong>Blossom algorithm</strong> (<a href="https://en.wikipedia.org/wiki/Edmonds%27s_matching_algorithm" rel="nofollow noreferrer">wikipedia</a>) to find a maximum matching. The idea is to start from an empty matching and iteratively transform it by mixing it with a kind of path called augmented path. When no such path exist anymore, the matching is maximal. One could argue that this algorithm can be implemented without really understanding why it works but finding an augmenting path is not completely obvious and one really need a precise grasp of the object to make it work without bug.</p>

<p>Dynamic programming algorithms also fall into this category. The <strong>change-making problem</strong> (<a href="https://en.wikipedia.org/wiki/Change-making_problem" rel="nofollow noreferrer">wikipedia</a>) is a good illustration of that. You have to be careful in defining the relation between the different records so that you are sure it works. The problem is actually also interesting because for some input, greedy approaches work. The fact that it works with the coin systems student are familiar with could mislead them to believe it will always work. Without proofs, people could be tempted to implement a wrong algorithm.</p>

<h1>Mastering an algorithm to make variations</h1>

<p>Mastering a good toolbox of classical algorithms is  essential to be able to design your own efficient algorithms. Knowing techniques such as binary search, fast exponentiation is inspiring to come up with optimization into more complex problems. Understanding the proof of their correctness or complexity is essential to be able to adapt them correctly in a different framework. This is similar to knowing the proof of a theorem in math. Without the proof, you are forced to use whatever statement of the theorem you were able to find in a textbook. With a proof, you can adapt the theorem, relax some hypothesis sometimes, change the underlying algebraic structure etc.</p>

<p><strong>Binary search</strong> (<a href="https://en.wikipedia.org/wiki/Binary_search" rel="nofollow noreferrer">wikipedia</a>) is a good and simple illustration of this fact. By understanding the proof of correctness, you know that you need an notion of order and a sorted array. This could be easily forgotten by someone who does not understand why the algorithm is correct. The proof of complexity is also important: the basic textbook will state that the search does <span class="math-container">$O(\log n)$</span> access to the array. But it is misleading and hide the fact that you also do <span class="math-container">$O(\log n)$</span> comparisons. Applying binary search for structures where equality is cheap but comparing is expensive tells you that it may be better to do a naive search or use some other techniques. <strong>Bloom's filters</strong> (<a href="https://en.wikipedia.org/wiki/Bloom_filter" rel="nofollow noreferrer">wikipedia</a>) are also a good illustration of this fact. You need to understand that the quality of the hash function is primordial in their performances.</p>

<p>Another example: the <strong>Bellman-Ford algorithm</strong> (<a href="https://en.wikipedia.org/wiki/Bellman-Ford_algorithm" rel="nofollow noreferrer">wikipedia</a>). It is not too hard to understand why it works. If you do not understand the proof, then it is just a shortest path algorithm. Now, if you understand the proof, you see that by changing the underlying semi-ring, you can compute other quantities such as the sum of weights of all path between two points in a DAG, the number of words of length <span class="math-container">$k$</span> accepted by a deterministic finite automaton etc.</p>

<h1>Complexity guarantees</h1>

<p>Some algorithms work by iteratively applying a function until a fix point is reached, the fix point being the solution to our problem. A proof of correction of these algorithms often gives you an upper bound on the number of needed iterations. Using it gives directly gives you an upper bound on the complexity or trade-off between complexity and quality of approximation. The Newton's method (<a href="https://en.wikipedia.org/wiki/Newton%27s_method" rel="nofollow noreferrer">wikipedia</a>) falls into this category, though it may be too mathematical. </p>

<h1>Toward implementations</h1>

<p>An algorithm may have many forms. From the general idea to concrete implementation. It is important to understand that they are many stages in the conception of the algorithm. Proving the correctness of each step is a big help to ensure a correct implementation in the end. Many textbook algorithms are not implementations but are given as pseudo-code and they still leave you room for optimization when implementing it. Proving the correctness of the algorithm is only the first step toward an efficient implementation. It gives an overview of the property we need in the  data structures, it can reveal parts that could be factorized together and grouped into a subfunction etc.</p>

<p>Dijkstra's algorithm (<a href="https://en.wikipedia.org/wiki/Dijkstra&#39;s_algorithm" rel="nofollow noreferrer">wikipedia</a>) is a very emblematic example of this fact. You can explain the main ideas before giving the details of each subfunction, before describing the heap datastructure to get good complexity guarantees. To finally converge toward an implementation.</p>

CC BY-SA 4.0
2020-01-03T16:24:34.863Z
2020-01-03T18:48:22.550Z
2020-01-03T18:48:22.550Z
holf
<p>In teaching Intro. Algorithms to undergrads, one of the most difficult tasks is to motivate why they need to know how to <em>prove</em> things about algorithms. (For many students, at least in many US universities, they may see some basic proofs in Discrete Mathematics, but Algorithms is often the first time they have to use proofs to reason about algorithms.) While I think I can do a decent job motivating this at an abstract level, concrete examples are much more convincing, hence my question:</p>

<blockquote>
  <p>I'm looking for concrete examples that show the value of proofs in algorithms.</p>
</blockquote>

<p>A couple questions already address this, and if you have answers to those, please add them there:</p>

<ul>
<li><a href="https://cstheory.stackexchange.com/q/40478/129">Examples of algorithms and proofs that seem correct, but aren't</a></li>
<li><a href="https://cs.stackexchange.com/q/29475/20219">How to fool the “try some test cases” heuristic: Algorithms that appear correct, but are actually incorrect</a></li>
</ul>

<p>However, I think there are other ways proofs can be valuable beyond the above. E.g., by working through the proof you can gain an insight that leads to a more efficient algorithm, or to an algorithm for a related problem, or to an idea for developing a better test suite to test your implementation, etc.</p>

<p>Some criteria:</p>

<ul>
<li><p>Answers here ideally shouldn't fit one of the questions above (as I said, please add an answer there if you have it)</p></li>
<li><p>Should be presentable to Intro. Algorithms students. While the proof itself need not be presentable, the <em>story</em> should be presentable (e.g. the statement of the problems involved, some idea of how the proof led to something that just "eyeballing correctness" would not have). If you are unsure about this point, go ahead and add it as an answer and I'll do my best to see if it can be presented to this audience.</p></li>
<li><p>Should be as natural as possible. Artificial examples are kinda okay, but real examples are much more motivating to students.</p></li>
<li><p>Note that I am talking here about abstract proofs for abstract algorithms, <em>not</em> formal (/automated/etc) proofs of algorithm implementations. As a litmus test, the ideas involved should not be language-specific.</p></li>
</ul>

<p>(While this question is not exactly research-level, I think it might get more answers here than on cs.SE, as I suspect the answers will come from  historical examples in the theory of algorithms that expert researchers on this site are more likely to be familiar with.)</p>

CC BY-SA 4.0
2020-01-02T17:32:07.337Z
Maybe this thought is interesting: On the search for an algorithm it often is helpful to find and prove some "structural properties" of the problem at hand which can then be used in an algorithm.
Daniel
CC BY-SA 4.0
2020-01-02T18:13:57.810Z
@Daniel: Indeed! That is often how I motivate many of the proofs in the course.
Joshua Grochow
CC BY-SA 4.0
2020-01-02T20:01:24.343Z
The pitch I make to my students is that you simply can't design algorithms (other than the obvious ones) without thinking about correctness.  One may think about it sloppily, of course, but nobody seriously proposes using a non-trivial algorithm without having some idea that it should work.  A proof of correctness is just a careful recording of a careful line of reasoning about correctness.  (That this needs to be pointed out at all is an artifact of the way students often learn about existing algorithms -- as methods that are known to work, where correctness is not really in question.)
Neal Young
CC BY-SA 4.0
2020-01-03T01:08:46.140Z
An issue related to the question is this: Examples of the value of _theorems_ for algorithms. See such examples in the earlier post https://cstheory.stackexchange.com/questions/21016/hard-looking-algorithmic-problems-made-easy-by-theorems
Andras Farago
CC BY-SA 4.0
2020-01-03T02:24:44.533Z
Basically second what Neal says. For any interesting problem where a correct algorithm is not "obvious" how would you go about designing an algorithm?
Chandra Chekuri
CC BY-SA 4.0
2020-01-03T13:26:10.643Z
Not sure if this fits with your goals, but basically every security vulnerability is a missing proof: somebody (the programmer) thought: this algorithms is safe, can't be used to steal credit card data etc because of <informal argument> ... Then somebody else finds a way to break the algorithm, because e.g. some control flow paths was ignored in the informal analysis.
Martin Berger
CC BY-SA 4.0
2020-01-03T19:20:49.277Z
@MartinBerger: This seems like a really good potential source of examples - if you know a specific example that would make a great answer! Unfortunately, most of the examples I know of in this space are either side channel attacks (the model was not inclusive enough) or language-specific (eg not taking into account the fact that C doesn't do bounds checking when accessing an array).
Joshua Grochow
CC BY-SA 4.0
2020-01-04T07:57:35.800Z
@MartinBerger: Maybe the Needham-Schroeder public key protocol? I've read that model checking is successfully used to find flaws in security protocols, but don't know a concrete example. https://en.m.wikipedia.org/wiki/Needham-Schroeder_protocol
Hermann Gruber
CC BY-SA 4.0
2020-01-04T11:30:02.160Z
@JoshuaGrochow Array bounds checking doesn't remove the underlying problem (use of wrong indices) but transforms the manifestation of the problem (into an exception), so moving from e.g. C to Java just changes the details of what needs to be proven (think: do you want your airplane's autopilot to throw an exception mid-flight).
Martin Berger
CC BY-SA 4.0
2020-01-04T11:31:47.310Z
@JoshuaGrochow Side channel attacks are especially good examples (I use the timing attack on the standard 3-line password checking algorithm as an example in teaching), because a suitable proof shows that the problem space is not well understood. (E.g. a Turing award was given for the definition of security of  public-key cryptosystems). The very question of what it means precisely to be secure makes sense only in the context of proof.
Martin Berger
CC BY-SA 4.0
2020-01-04T11:38:07.533Z
@HermannGruber Most  informally specified crypto protocols have been found to have gaps. Most verified protocols have been found to have gaps later (because the verification worked on a higher level of abstraction than the implementation), whence Microsoft's [Project Everest](https://project-everest.github.io/). Coincidentally essentially all verified cryptography relies on unproven cryptographic hardness assumptions, like the hardness of the RSA problem.
Martin Berger
<ds.algorithms><proofs><teaching>
Examples of the value of proofs for algorithms
Joshua Grochow
# Examples of the value of proofs for algorithms

(Asked by: username_0 on 2020-01-02)

In teaching Intro. Algorithms to undergrads, one of the most difficult tasks is to motivate why they need to know how to *prove* things about algorithms. (For many students, at least in many US universities, they may see some basic proofs in Discrete Mathematics, but Algorithms is often the first time they have to use proofs to reason about algorithms.) While I think I can do a decent job motivating this at an abstract level, concrete examples are much more convincing, hence my question:

> I'm looking for concrete examples that show the value of proofs in algorithms.

A couple questions already address this, and if you have answers to those, please add them there:

* [Examples of algorithms and proofs that seem correct, but aren't](https://cstheory.stackexchange.com/q/40478/129)
* [How to fool the “try some test cases” heuristic: Algorithms that appear correct, but are actually incorrect](https://cs.stackexchange.com/q/29475/20219)

However, I think there are other ways proofs can be valuable beyond the above. E.g., by working through the proof you can gain an insight that leads to a more efficient algorithm, or to an algorithm for a related problem, or to an idea for developing a better test suite to test your implementation, etc.

Some criteria:

* Answers here ideally shouldn't fit one of the questions above (as I said, please add an answer there if you have it)
* Should be presentable to Intro. Algorithms students. While the proof itself need not be presentable, the *story* should be presentable (e.g. the statement of the problems involved, some idea of how the proof led to something that just "eyeballing correctness" would not have). If you are unsure about this point, go ahead and add it as an answer and I'll do my best to see if it can be presented to this audience.
* Should be as natural as possible. Artificial examples are kinda okay, but real examples are much more motivating to students.
* Note that I am talking here about abstract proofs for abstract algorithms, *not* formal (/automated/etc) proofs of algorithm implementations. As a litmus test, the ideas involved should not be language-specific.

(While this question is not exactly research-level, I think it might get more answers here than on cs.SE, as I suspect the answers will come from historical examples in the theory of algorithms that expert researchers on this site are more likely to be familiar with.)

**Tags:** ds.algorithms, proofs, teaching
> **Comments:**
> **username_1**: Maybe this thought is interesting: On the search for an algorithm it often is helpful to find and prove some "structural properties" of the problem at hand which can then be used in an algorithm.  
> **username_0**: @Daniel: Indeed! That is often how I motivate many of the proofs in the course.  
> **username_2**: The pitch I make to my students is that you simply can't design algorithms (other than the obvious ones) without thinking about correctness.  One may think about it sloppily, of course, but nobody seriously proposes using a non-trivial algorithm without having some idea that it should work.  A proof of correctness is just a careful recording of a careful line of reasoning about correctness.  (That this needs to be pointed out at all is an artifact of the way students often learn about existing algorithms -- as methods that are known to work, where correctness is not really in question.)  
> **username_3**: An issue related to the question is this: Examples of the value of _theorems_ for algorithms. See such examples in the earlier post https://cstheory.stackexchange.com/questions/21016/hard-looking-algorithmic-problems-made-easy-by-theorems  
> **username_4**: Basically second what Neal says. For any interesting problem where a correct algorithm is not "obvious" how would you go about designing an algorithm?  
> **username_5**: Not sure if this fits with your goals, but basically every security vulnerability is a missing proof: somebody (the programmer) thought: this algorithms is safe, can't be used to steal credit card data etc because of <informal argument> ... Then somebody else finds a way to break the algorithm, because e.g. some control flow paths was ignored in the informal analysis.  
> **username_0**: @MartinBerger: This seems like a really good potential source of examples - if you know a specific example that would make a great answer! Unfortunately, most of the examples I know of in this space are either side channel attacks (the model was not inclusive enough) or language-specific (eg not taking into account the fact that C doesn't do bounds checking when accessing an array).  
> **username_6**: @MartinBerger: Maybe the Needham-Schroeder public key protocol? I've read that model checking is successfully used to find flaws in security protocols, but don't know a concrete example. https://en.m.wikipedia.org/wiki/Needham-Schroeder_protocol  
> **username_5**: @JoshuaGrochow Array bounds checking doesn't remove the underlying problem (use of wrong indices) but transforms the manifestation of the problem (into an exception), so moving from e.g. C to Java just changes the details of what needs to be proven (think: do you want your airplane's autopilot to throw an exception mid-flight).  
> **username_5**: @JoshuaGrochow Side channel attacks are especially good examples (I use the timing attack on the standard 3-line password checking algorithm as an example in teaching), because a suitable proof shows that the problem space is not well understood. (E.g. a Turing award was given for the definition of security of  public-key cryptosystems). The very question of what it means precisely to be secure makes sense only in the context of proof.  
> **username_5**: @HermannGruber Most  informally specified crypto protocols have been found to have gaps. Most verified protocols have been found to have gaps later (because the verification worked on a higher level of abstraction than the implementation), whence Microsoft's [Project Everest](https://project-everest.github.io/). Coincidentally essentially all verified cryptography relies on unproven cryptographic hardness assumptions, like the hardness of the RSA problem.  

---

## 3 answers

### Answer by username_3 on 2020-01-02. Score: 5

Here is a natural problem from graph theory where the proof and the algorithm are closely intertwined. In my view, one can discover this algorithm only via thinking about the proof and the algorithm "in parallel." The task is this:

**Input:** An undirected graph.

**Task:** Find a subgraph with maximum edge-connectivity.

***Note:*** What makes the task non-trivial is that a subgraph can have larger edge-connectivity than the whole graph. Since there are exponentially many subgraphs, it would take exponential time to check all of them to find the most connected one, even though we can compute the edge-connectivity of any graph in polynomial time.

Below is a part of a lecture note about solving this problem. It shows that the task can be solved in polynomial time, using a subroutine that finds a minimum cut (which is well know to be doable in polynomial time). For short, edge-connectivity is just called connectivity, and is denoted by $\lambda(G)$.

[![Finding a subgraph with maximum edge connectivity](https://i.sstatic.net/azaAv.png)](https://i.sstatic.net/azaAv.png)

> **Comments:**
> **username_0**: This is a nice example problem! I might see if I can use it when we do divide & conquer (we typically do that before mincut, but I can give them mincut as an oracle and it will also be nice foreshadowing). In terms of the proof though, if you just want polynomial time, isn't it trivial that mincut is called at most O(m) times (m=# edges), since each time you call it you remove at least one edge?  
> **username_3**: @JoshuaGrochow Yes, you are perfectly right! Even if the graph has exponentially many edges (it is possible, due to parallel edges, which were not excluded), your argument still carries over, since each min cut call removes at least one full bundle of edges (=all edges between two nodes), and there are at most $n(n-1)/2$ such bundles. However, the $f(n)\leq n-1$ bound is tighter. In fact, it can hold with equality, as shown by the example of an induced path.  

---

### Answer by username_7 on 2020-01-02. Score: 2

A practical answer: In my career I encountered a few scenarios, some with my direct involvement, where I had to prove that my algorithm performs just as good as the currently best known possible. There are many examples where such knowledge can have a direct effect on one's career... In my experience, making a good claim at a design review meeting or to your direct boss can sometimes be more important than actual implementation.
Some examples:
The first "trivial" example was at the very beginning of my career.
I was the only "engineer" in the company.
The internet was only at it's beginning and they wrote code for median finding by first sorting the numbers and then take the center element.
I actually had to explain why the linear time algorithm actually works in linear time...
The second one involved 2D correlation for motion detection.
The idea is too long to explain here, but I had to explain (prove) why the specific conditions of the problem makes it possible for my algorithm to run faster than the obvious one.


---

### Answer by username_8 on 2020-01-03. Score: 2

I see several advantages of mastering the proof of correctness and complexity of an algorithm. I list them below and illustrate with a concrete example. I tried to stay in the domain of classical textbook algorithms.

# Understanding why the algorithm works

Certainly the most obvious reason of having proofs. Many algorithms exploit some structure in the problem in a non obvious way. Without proving their correction, there is no way to really understand why it works. Without understanding this, there is no way of really implementing it.

One example of such algorithm is the **Blossom algorithm** ([wikipedia](https://en.wikipedia.org/wiki/Edmonds%27s_matching_algorithm)) to find a maximum matching. The idea is to start from an empty matching and iteratively transform it by mixing it with a kind of path called augmented path. When no such path exist anymore, the matching is maximal. One could argue that this algorithm can be implemented without really understanding why it works but finding an augmenting path is not completely obvious and one really need a precise grasp of the object to make it work without bug.

Dynamic programming algorithms also fall into this category. The **change-making problem** ([wikipedia](https://en.wikipedia.org/wiki/Change-making_problem)) is a good illustration of that. You have to be careful in defining the relation between the different records so that you are sure it works. The problem is actually also interesting because for some input, greedy approaches work. The fact that it works with the coin systems student are familiar with could mislead them to believe it will always work. Without proofs, people could be tempted to implement a wrong algorithm.

# Mastering an algorithm to make variations

Mastering a good toolbox of classical algorithms is essential to be able to design your own efficient algorithms. Knowing techniques such as binary search, fast exponentiation is inspiring to come up with optimization into more complex problems. Understanding the proof of their correctness or complexity is essential to be able to adapt them correctly in a different framework. This is similar to knowing the proof of a theorem in math. Without the proof, you are forced to use whatever statement of the theorem you were able to find in a textbook. With a proof, you can adapt the theorem, relax some hypothesis sometimes, change the underlying algebraic structure etc.

**Binary search** ([wikipedia](https://en.wikipedia.org/wiki/Binary_search)) is a good and simple illustration of this fact. By understanding the proof of correctness, you know that you need an notion of order and a sorted array. This could be easily forgotten by someone who does not understand why the algorithm is correct. The proof of complexity is also important: the basic textbook will state that the search does $O(\log n)$ access to the array. But it is misleading and hide the fact that you also do $O(\log n)$ comparisons. Applying binary search for structures where equality is cheap but comparing is expensive tells you that it may be better to do a naive search or use some other techniques. **Bloom's filters** ([wikipedia](https://en.wikipedia.org/wiki/Bloom_filter)) are also a good illustration of this fact. You need to understand that the quality of the hash function is primordial in their performances.

Another example: the **Bellman-Ford algorithm** ([wikipedia](https://en.wikipedia.org/wiki/Bellman-Ford_algorithm)). It is not too hard to understand why it works. If you do not understand the proof, then it is just a shortest path algorithm. Now, if you understand the proof, you see that by changing the underlying semi-ring, you can compute other quantities such as the sum of weights of all path between two points in a DAG, the number of words of length $k$ accepted by a deterministic finite automaton etc.

# Complexity guarantees

Some algorithms work by iteratively applying a function until a fix point is reached, the fix point being the solution to our problem. A proof of correction of these algorithms often gives you an upper bound on the number of needed iterations. Using it gives directly gives you an upper bound on the complexity or trade-off between complexity and quality of approximation. The Newton's method ([wikipedia](https://en.wikipedia.org/wiki/Newton%27s_method)) falls into this category, though it may be too mathematical.

# Toward implementations

An algorithm may have many forms. From the general idea to concrete implementation. It is important to understand that they are many stages in the conception of the algorithm. Proving the correctness of each step is a big help to ensure a correct implementation in the end. Many textbook algorithms are not implementations but are given as pseudo-code and they still leave you room for optimization when implementing it. Proving the correctness of the algorithm is only the first step toward an efficient implementation. It gives an overview of the property we need in the data structures, it can reveal parts that could be factorized together and grouped into a subfunction etc.

Dijkstra's algorithm ([wikipedia](https://en.wikipedia.org/wiki/Dijkstra's_algorithm)) is a very emblematic example of this fact. You can explain the main ideas before giving the details of each subfunction, before describing the heap datastructure to get good complexity guarantees. To finally converge toward an implementation.


---

