All programming is proof. You just don't often know what exactly it is you're proving.
Anyway, the point is moot: software is not that reliable. It's good at the common case, and is very brittle at the edge cases. That's my experience anyway.
Anyway, the point is moot: software is not that reliable. It's good at the common case, and is very brittle at the edge cases. That's my experience anyway.
The language (spec) is my set of axioms, the standard library existing theorems, and my program the proof.
It's kinda drab now that I think about it, but for a 'firing from the hip' answer I still stand by it.
In other words, the Curry–Howard correspondence is the observation that two families of formalisms that had seemed unrelated—namely, the proof systems on one hand, and the models of computation on the other—were, in the two examples considered by Curry and Howard, in fact structurally the same kind of objects.
If one now abstracts on the peculiarities of this or that formalism, the immediate generalization is the following claim: a proof is a program, the formula it proves is a type for the program. More informally, this can be seen as an analogy that states that the return type of a function (i.e., the type of values returned by a function) is analogous to a logical theorem ... and that the program to compute that function is analogous to a proof of that theorem. This sets a form of logic programming on a rigorous foundation: proofs can be represented as programs, and especially as lambda terms, or proofs can be run.
(Of course, in the context of those job interviews you mentioned, this sort of thing would probably be overkill, unless the job involved functional-programming...in which case, though, they might well not have asked you how your "skills in mathematics would transition to programming" in the first place :-) ).
[0] https://en.wikipedia.org/wiki/Curry–Howard_correspondence