News for hackers. Stuff that matters.

A comment on Mathematicians are chronically lost and confused (2014). Parent comment

Re:Mathematicians are chronically lost and confused (2014) by mindcrime on Friday June 10, 2016 @03:22PM (#11879209)
In my limited experience I believe one advantage programming has over mathematics in terms of self learning is that in programming one is more likely to know that a program works/doesn't work versus knowing whether your conception of an abstract definition or theorem is correct.

I've often wondered if automated theorem provers (Coq and the like) could be useful for this. Sure, it requires learning Coq (or Agda or ACL2 or whatever), but it seems that it might be worthwhile just as a way to sanity check one's work - somewhat akin to the way a compiler "checks your work" when programming.

[ Parent | on HN ]
Re:Mathematicians are chronically lost and confused (2014) by agentultra on Friday June 10, 2016 @06:29PM (#11880637)
Insanely useful. I believe it should be state of the art. Even model checkers are vastly more useful than nothing.
[ Parent | on HN ]