Which packages/practices are relevant for writing Structured Derivations? (similar to Dijkstra's calculational style of proofs)

I'd be tempted to use a sequence of itemize and enumerate environment, using the enumitem package to help with formatting

In the code below I've used the resume feature provided by the enumitem package to help keep the numbering of the enumerate environment without having to hardcode any of the numbers.

I've also used the optional argument of the \item command, which can be used, for example

\item[$\Vdash$]

If you plan to use this a lot though, you could always make this into a \newcommand

\documentclass{article}
\usepackage{geometry}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{enumitem}

% global settings for enumerate environment
\setlist[enumerate]{label*=(\arabic*),leftmargin=0mm}

% itemize environment, when at nested depths 2, 3, 4
\setlist[itemize,2]{label=\textbullet,leftmargin=1cm}
\setlist[itemize,3]{label=\textbullet,leftmargin=1cm}
\setlist[itemize,4]{label=\textbullet,leftmargin=1cm}

\begin{document}
\begin{itemize}
    \item Show that $f$ is continuous at $x_0$, when
        \begin{enumerate}
            \item\label{item:range} $f(x)=\sqrt{x}$ when $x\geq 0$, and
            \item\label{item:pos} $x_0>0$
        \end{enumerate}
    \item[$\Vdash$] $f$ is continuous at $x_0$
    \item[$\equiv$] $\{\text{definition of continuity}\}$

            $(\forall\epsilon>0\cdot \exists\delta>0\cdot\forall x\geq 0\cdot |x-x_0|<\delta\Rightarrow|f(x)-f(x_0)|<\epsilon)$
    \item[$\equiv$] $\{\text{choose arbitrary }\epsilon \text{generilization rule}\}$
    \begin{itemize}
        \item Show that $(\exists\delta>0\cdot\forall x\geq 0\cdot |x-x_0|<\delta\Rightarrow |f(x)-f(x_0)|<\epsilon)$, when
        \begin{enumerate}[resume]
            \item $\epsilon>0$
        \end{enumerate}
        \item[$\Vdash$] $\{\text{find a suitable value for } \delta\text{ witness rule}\}$
        \begin{itemize}
            \item Show that $\delta>0\wedge(\forall x\geq 0\cdot|x-x_0|<\delta\Rightarrow|f(x)-f(x_0)|<\epsilon)$, when
            \begin{enumerate}[resume]
                \item $\delta=?$ $\sharp$ $\delta=\epsilon\cdot\sqrt{x_0}$
            \end{enumerate}
            \item[$\Vdash$] $\{\text{show the two conjuncts separately, use generalization rule for second conjunct}\}$
            \begin{itemize}
                \item Show that $|f(x)-f(x_0)|<\epsilon$, when
                \begin{enumerate}[resume]
                    \item\label{item:xnonneg} $x\geq 0$, and
                    \item $|x-x_0|<\delta$
                \end{enumerate}
                \item[$\Vdash$] $|f(x)-f(x_0)|$
                \item[$=$] $\{$assumption \ref{item:range}, $f(x)$ and $f(x_0)$ are defined by assumptions \ref{item:xnonneg} and \ref{item:range}$\}$
                \item[] $|\sqrt{x}-\sqrt{x_0}|$
                \item[$=$] $\{$extend with conjugate value for $\sqrt{x}-\sqrt{x_0}$, i.e., with $\sqrt{x}+\sqrt{x_0}>0$$\}$
                \item[] $\dfrac{|x-x_0|}{\sqrt{x}+\sqrt{x_0}}$
                \item[$\leq$] $\{$make divisor smaller, $\sqrt{x}\geq 0$ $\}$
            \end{itemize}
        \end{itemize}
    \end{itemize}
\end{itemize}
\end{document}

You may be interested in a package written by Leslie Lamport, pf2, which is used to produced a structured proof that looks pretty similar to the style used by Dijkstra. The package is just a single .sty file and does not seem to be hosted on CTAN, but you can find it here: http://lamport.azurewebsites.net/latex/latex.html.

The style provided by this package would look like one of these two columns below (you get the freedom to change the styles of the numbering and indentation). I think after some tweaking you may be able to achieve the desired aesthetic. Well, arguably easier than the heavy-lifting using a bunch of nested itemize and enumerate.

Edit: After some googling I don't find an elegant way of creating nested lists with ease. Markdown + KaTeX (or MathJax) and LaTeX conversion thru pandoc may be close to that but you only get a limited set of LaTeX commands supported within the Markdown environment.

Fokkinga posted such a package in January 2015; it's called calculation.

It follows the approach of eqnarray somehow (so says the documentation). So fractions and big operators get cramped. Otherwise, it's nice.