Good software propagates its own correctness

Writing good software code is an exercise in applied schizophrenia. You need to please two radically disctinct audiences. The first audience is the compiler and the runtime. A patient and diligent audience that takes your writing to the letter. The second audience is your peers, fellow software engineers. On the plus side, this audience tries to adhere to the spirit of your writing; on the minus side, they can misunderstand your writing entirely.

Good software propagates its own correctness (with an application to Bitcoin)

PDF at https://blog.vermorel.com/pdf/correctness-propagation-2018-04-26.pdf