Implementing Tarjan's strongly connected components algorithm in a language without exceptions or undefined behavior

Question

I asked this question on Stack Overflow, but I have not obtained an actual answer to the question.

---

Tarjan's strongly connected components algorithm is stunningly beautiful, and inexpressible in a literal way in any programming language that I know of.

Allow me to refer to the pseudocode in the Wikipedia article. The problem is with the code that pops the strongly connected component we just found from the auxiliary stack:

// If v is a root node, pop the stack and generate an SCC
if (v.lowlink = v.index) then
  start a new strongly connected component
  repeat
    w := S.pop()
    w.onStack := false
    add w to current strongly connected component
  while (w != v)
  output the current strongly connected component
end if

The instruction w := S.pop() is unsafe, because, as far as the programming language's static semantics knows or cares, S could be empty. (Of course, a human programmer can easily tell that S will not be empty, because we are only popping S until we find v, which is initially contained in S.) Hence, a compiler for a memory safe language will emit code that

1. Checks whether S is empty.
2. Raises an exception if the stack is empty.
3. Pops and returns the stack's top element otherwise.

I am not too worried about the (negligible) performance impact of the useless test of emptiness. (Thus, “rewrite it in a memory-unsafe language” is not an answer.) However, I am concerned with the fact I cannot communicate an important invariant in a way that the compiler can treat as actionable information.

My questions are:

1. Am I overlooking some way in which I can communicate to the compiler the fact that S contains v?

2. If the answer to the first question is negative, is there a proof that I can't communicate this fact to the compiler?

---

EDIT: I am starting to suspect that the key to solving this conundrum is to use the same tricks I used to work around the lack of polymorphic recursion in SML without introducing redundant safety checks, but I need to properly write this down.

Answer 1

There will always be situations where we can see there is a complex invariant but the compiler cannot derive it. Type systems are sound but not complete: not all invariants can be expressed in the type system. So this isn't something specific to Tarjan's algorithm; it is a general fact of life when working in a type system -- sometimes the compiler will insert type checks that the programmer can tell won't be necessary, and similarly, as a programmer you might need to insert type checks that you can tell won't be necessary.

Answer 2

By a happy coincidence, people (Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz and Laurent Thery) have completed formally verified implementations of Tarjan's algorithm in various formal systems!

The paper, titled "Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle", can be found, e.g. here.

One step of proving correctness in these systems is necessarily excluding the exceptions and undefined behavior you mention, so the article should be very relevant!

The Why3 implementation is probably the closest one to the Wikipedia pseudo-code.