3 ms·
Most programmers don't have enough previous experience proving things so this is unnatural for them. It is sadly impossible to require programmers to have been
by kccqzy 2y ago
Most programmers don't have enough previous experience proving things so this is unnatural for them. It is sadly impossible to require programmers to have been a math major to get them the mental facility to work with these languages.
- trealira 2y agoAt my university, all majors of computer science have to take a course in discrete math, which involves writing a couple different types of math proofs using proof by induction (including strong induction) and proof by contradiction. However, that was the only class I've ever taken where I've had to write proofs regularly. Anyway, I think that, at a minimum, at least one class like that should be part of every CS major's education, if it isn't already. That way, proofs are less intimidating, and things like Coq and Isabelle/HOL are less intimidating.
- kccqzy 2y agoI agree with you, but the ship has sailed to retroactively require all programmers to have such experience. Also, the typical introductory discrete math course likely doesn't require writing proofs in a language precise enough to be formalized. I would think that we need at least one more introductory course to logic (first order logic, Peano axioms) and an introductory course to type systems (structural induction, progress and preservation, etc).
- trealira 2y agoWe also learned some first order logic, enough to write the proofs in formal language, though we didn't learn anything about type systems. You're probably right about the ship having sailed, though. It's probably harder to get people to learn new things when they haven't been in school for a long time.