How can I prove the result of a long computation with a short string? I have a simple program F (think of a cellular automaton) that, when executed in some input X, takes a while to complete and returns a short result (a hash function, for example). How do I produce a short string that proves the result F(X) = Y without requiring the verifier to run the entire computation?

I'm aware of zk-snarks, but I couldn't a simple, practical "get started" guide to them. Moreover, they might be overkill for this since I don't need any privacy.
There are several option - none of which is trivial to implement.

A bit of background first. Essentially, verifiable delegation of computation boils down to being able to prove relations between inputs and outputs, so that the verification time is way smaller than the computation time, for relations that can be computed in polynomial time. In contrast, the famous SNARGs are way more powerful, as they also allow to prove any NP statement, even those that are not known to be computable in polynomial time. So in a sense, delegating computation is "easier" than constructing SNARGs. However, two remarks are in order:


A very large effort has been devoted to the analysis and construction of SNARGs, even leading to some implementations (e.g. zcash). Therefore, it might be that the current best way of verifying delegated computation in practice goes through SNARGs
A sense in which SNARGs are harder than verifiable computation is with respect to the underlying assumptions: while we have strong indications that SNARGs require non-standard assumptions, we know how to base verifiable computation on standard assumptions. But if you are looking for a practical solution, you might well not care about the theoretical issues of the underlying assumptions.


For those reasons, even in SNARG is an overkill from a theoretical point of view, it is not necessarily the case if what you care about is practice, and you can easily find some implementations (there are more recent ones, such as the famous Pinocchio, or the even more recent Geppetto).

That being said, there are several natural approaches for delegation of computation. The first that comes to mind is this approach, which is the seminal paper on the topic of delegation, and that works for restricted classes of computation. This approach was refined several time, culminating with this beautiful paper that gives a very satisfying solution for delegating evaluation of boolean circuit, with reasonable efficiency. I believe they have implementations, I do not know how easy it is to find and reuse these implementations.

The second, that I only mention for the sake of completeness, is to use techniques for batch verification: the prover evaluate the same program $P$ on many inputs $x_1, \cdots, x_n$, in time $O(sn)$ ($s$ being the time needed to evaluate $P$ on a single input) and the verifier can check the correctness of all computations in time $O(s + n)$, instead of $O(sn)$.

Another natural approach (see also this paper, this paper, and papers that reference them on Google scholar) for delegation of computation essentially requires to ask the server to perform the computation in the encrypted domain, via fully homomorphic encryption. It is based on homomorphic MACs, which can be constructed from FHE. From my understanding, they are conceptually quite simple - you essentially have to execute the computation several time in the encrypted domain, and there is an easy check for the verifier. The main issue is the cost of using FHE - but if your circuit is small enough, using this recent FHE scheme (see also the follow up) which performs bootstrapping in less than 20ms, this might be quite feasible. For more restricted computations, one can also avoid using FHE.

I've not read it yet, but if you have access to the ACM digital library, there was a recent survey on the subject of verifiable computation, by one of the leading researchers in the area (Rosario Gennaro), called "Verifiable Outsourced Computation: A Survey".