In addition to the recent Coq-related efforts mentioned by others, one should consider the Isabelle/HOL and ACL2 communities. Isabelle/HOL does get used in industry, e.g. NICTA/Data61's formalization of sel4 kernel. See talks by J Moore on ACL2 and by Gerwin Klein on sel4 at the recent Royal Society discussion meeting on "verified trustworthy software systems"
https://royalsociety.org/events/2016/04/software-systems/There are also (relative) success stories in mathematics, e.g. the GAP system:
www.gap-system.org/None of this is to say that software credit and maintenance (and development to the level of maturity needed for acceptance in the mathematical community) is a solved problem, but there are other solution attempts that can be considered to better understand the problem. Fundamentally, what is needed is resources, whether this means money from funding agencies, investment capital, or donations of free time from open source contributors. In each case, persuasion and leadership is needed, but what form this takes seems very situation-dependent and there is no guarantee that the needed model will fit anyone's pre-existing vision of a "successful [academic] career".
--James
PS. I also enjoyed the comic.