Nice to hear. I had similar moments of epiphany while taking a course on abstract algebra and writing down some theorems in the form of Agda definitions. As y

Nice to hear. I had similar moments of epiphany while taking a course on abstract algebra and writing down some theorems in the form of Agda definitions. As you may know, Agda is a Haskell-inspired language that has an even more powerful type system that makes it possible to define arbitrarily strong types, so that for instance you can define the type of a function that sorts a list—and then know confidently that any implementation of that type does indeed sort a list. Anyway, when learning Agda, one comes across the notion that programs and proofs are in some sense the same thing. In other words that the code for a function can be read as a proof that the type of that function is inhabited. This seemed to me kind of bizarre and magical at first... The more I thought about it, the more it made real sense, and not only that, it helped me understand proofs in a much more intuitive way. Before, if you had asked me what a proof is, I might have said "it's a very strict way to argue that a statement really is true." I didn't know that such proofs can be given formal structure... I couldn't really explain how to relate it to programming or functions... But now that I've to some degree internalized the notion, if you ask me what a proof is, I might say it's an unambiguous description of how to transform an input into an output. If you call the input P and the output Q, then P is a premise and Q is a conclusion, and the proof is the "arrow" P -> Q that through some well-defined sequence of "truth-preserving transformations" gives you knowledge of Q assuming nothing but P (and some fundamental axioms). And in the world of programming, P is an input argument and Q is a resulting value, while the "arrow" P -> Q is a well-defined sequence of correct transformation that produces a Q-value given only a P-value (and some fundamental primitive functions). So in this sense you can say that the implementation of a function is actually a kind of logical argument. If you want to make use of this insightful connection (the "Curry-Howard equivalence"), however, your programming language needs to be pretty strict. If your P -> Q argument suddenly throws a null pointer exception, it's not much of an argument—it means your claim of being able to produce a Q given P is false. This connection really helped me to understand both proofs and programs in a deeper way.