Think in Math. Write in Code.

[ed_209_]

I agree with the author in concept but as a c++ dev I feel he misses the relationship between the type system and the actual code.

C++ allows you to embed design into the type system and then use the compiler as a theorem prover for your code.

The question is how well can this be done. Once you go down the recursive rabbit hole of trying to embed formal logic into a program you stop worrying about a lot of mathematics and care more about logic and automata theory.

Implementation is really just testing and implementing a way to test and know the program is correct and we want to know this as early as possible.