> The specification is a lot smaller than the code, and so it's easier to read and manually verify that it's correct.

>> How is that the case in this specific example? It looks a lot harder to check for correctness.

Author here.

Here is the specification for the stochastic backpropagation algorithm:

https://github.com/dselsam/certigrad/blob/master/src/certigr...

The preconditions do not need to be inspected carefully because we prove that the models of interest satisfy them (example: https://github.com/dselsam/certigrad/blob/master/src/certigr...)

Here is the part of the specification that needs to be inspected carefully:

https://github.com/dselsam/certigrad/blob/master/src/certigr...

The syntax may seem strange to those unfamiliar with Lean, and a few of the functions involved may not be self-explanatory without reading their definitions, but the statement is conceptually simple: the stochastic backpropagation algorithm correctly computes unbiased estimates of the gradient of the expected loss.

It is subjective, but I personally think that this specification is vastly easier to understand and to check for correctness than the actual implementation of the stochastic backpropagation algorithm.