6 ms·
They can be interpreted as math, but they aren't really. If you are using Coq or something verified it can be, but especially when you are using a dynamic langu
by ArtB 14y ago
They can be interpreted as math, but they aren't really. If you are using Coq or something verified it can be, but especially when you are using a dynamic language and you have no idea of the types of objects that will be passed as parameters or when you are just slapdashing bits of scripts together (like, "hmm, that failed, maybe I should just +1 to it?") it's hard to compare that to the rigorous discipline called math.
- zeteo 14y agoMath went on for millenia without computerized proof checking and yes, some of those proofs were buggy. The difference between a professional mathematician and a software engineer is no more than that between a C and a Prolog programmer. Anyone who has written both proofs by induction and recursive programs can easily see the correspondence, even without the Curry-Haskell proof that the correspondence exists.