I am slightly confused about what formal derivatives over finite fields mean.
Example 1: Consider $f(x)=x^3-2\in \mathbb{F}_7[x]$.
By checking each element of $\mathbb{F}_7$ we easily see that this is irreducible. What about separable? Can we look at the formal derivative $f’(x)=3x^2$ which has a double zero at $0$ and hence gcd$(f,f’)=1$ and so $f(x)$ is separable?
Example 2: Consider $f(x)=x^p-x+1\in\mathbb{F}_p[x]$.
Observe that if $\alpha$ is a root then $\alpha +a$ is a root for any $a\in\mathbb{F}_p$ (because $(\alpha +a)^p=\alpha^p+a^p$). Hence has $0$ is not a root, $f$ is irreducible.
Now $f$ is separable because we have $p$ distinct roots. Can we show this also by the formal derivative? What is the formal derivative here?
Yes to your first question, and $$(x^p-x+1)'=px^{p-1}-1=-1\pmod p$$ so the pol. is separable (as is any irreducible pol. over any field of characteristic zero or over any finite field)