Thirty-Three Years of Mathematicians and Software Engineers: A Case Study of Domain Expertise and Participation in Proof Assistant Ecosystems
As technical computing software, such as MATLAB and SciPy, has gained popularity, ecosystems of interdependent software solutions and communities have formed around these technologies. The development and maintenance of these technical computing ecosystems requires expertise in both software engineering and the underlying technical domain. The inherently interdisciplinary nature of these ecosystems presents unique challenges and opportunities that shape software development practices. Proof assistants, a type of technical computing software, aid users in the creation of formal proofs. In order to examine the influence of the underlying technical domain — mathematics — on the development of proof assistant ecosystems, we mined participant activity data from the code repositories and social channels of three popular proof assistants: Lean, Coq, Isabelle. Despite having a shared technical domain, we found little cross-pollination between contributors to the proof assistants. Additionally, we found that most long-term developers focused solely on technical work and did not participate in official social channels. We also found that proof assistant developers specialized into technical subfields. However, the proportion of specialists varied between ecosystems. We did not find evidence that these specialties contributed to fractures within the ecosystems. We discuss the implications of these results on the long-term health and sustainability of proof assistant ecosystems.
Mon 15 AprDisplayed time zone: Lisbon change
11:00 - 12:30 | Ecosystems, Reuse and APIs & TutorialsData and Tool Showcase Track / Technical Papers / Tutorials at Almada Negreiros Chair(s): Mahmoud Alfadel University of Waterloo, Ayushi Rastogi University of Groningen, The Netherlands | ||
11:00 12mTalk | Thirty-Three Years of Mathematicians and Software Engineers: A Case Study of Domain Expertise and Participation in Proof Assistant Ecosystems Technical Papers Gwenyth Lincroft Northeastern University, Minsung Cho Northeastern University, Mahsa Bazzaz Northeastern University, Katherine Hough Northeastern University, Jonathan Bell Northeastern University Pre-print Media Attached | ||
11:12 12mTalk | Boosting API Misuse Detection via Integrating API Constraints from Multiple Sources Technical Papers Can Li Nanjing University of Aeronautics and Astronautics, Jingxuan Zhang Nanjing University of Aeronautics and Astronautics, Yixuan Tang Nanjing University of Aeronautics and Astronautics, Zhuhang Li Nanjing University of Aeronautics and Astronautics, Tianyue Sun Nanjing University of Aeronautics and Astronautics | ||
11:24 6mTalk | Availability and Usage of Platform-Specific APIs: A First Empirical Study Technical Papers Pre-print Media Attached File Attached | ||
11:30 4mTalk | AndroLibZoo: A Reliable Dataset of Libraries Based on Software Dependency Analysis Data and Tool Showcase Track Jordan Samhi CISPA Helmholtz Center for Information Security, Tegawendé F. Bissyandé University of Luxembourg, Jacques Klein University of Luxembourg | ||
11:34 4mTalk | Goblin: A Framework for Enriching and Querying the Maven Central Dependency Graph Data and Tool Showcase Track Damien Jaime Sorbonne Université - Lip6 - SAP, Joyce El Haddad Paris Dauphine-PSL Université, CNRS, LAMSADE, Pascal Poizat Université Paris Nanterre & LIP6 Pre-print File Attached | ||
11:38 4mTalk | Dataset: Copy-based Reuse in Open Source Software Data and Tool Showcase Track Mahmoud Jahanshahi Research Assistant, University of Tennessee Knoxville, Audris Mockus The University of Tennessee & Vilnius University Pre-print | ||
11:45 45mTalk | Mining Our Way Back to Incremental Builds for DevOps Pipelines Tutorials Shane McIntosh University of Waterloo Pre-print |