> 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

> 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/certigrad/backprop_correct.lean#L13-L25 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/certigrad/aevb/grads_correct.lean#L20-L27 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/certigrad/backprop_correct.lean#L23-L25 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.