long time no see! there's a couple levels there: rote translating pseudocode into your target language isn't likely to pan out well. so instead you run the p

long time no see! there's a couple levels there: rote translating pseudocode into your target language isn't likely to pan out well. so instead you run the pseudocode in your mind, develop an intuition on how it works, and that's the "replication" bit this post talks about with reviewing math papers. but both the pseudocode and your code will likely have edge cases you didn't handle. this isn't a problem for math - that's the category of common trivial/easily fixable proof errors that don't really affect the paper. but they're a problem for machines that run them literally. maybe a good compromise strategy for formal verification is to declare the insight of the algorithm - recurrence relation or whatever - as an axiom, and then use the prover to whack the tricky edge cases.