skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.


Title: Artifact to Accompany "33 Years of Mathematicians and Software Engineers: A Case Study of 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.This artifact contains the scripts and dataset that support an MSR 2024 article.  more » « less
Award ID(s):
2100015
PAR ID:
10496129
Author(s) / Creator(s):
; ; ; ;
Publisher / Repository:
figshare
Date Published:
Subject(s) / Keyword(s):
Empirical software engineering
Format(s):
Medium: X Size: 93199126 Bytes
Size(s):
93199126 Bytes
Sponsoring Org:
National Science Foundation
More Like this
  1. The rapid adoption of generative AI in software development has impacted the industry, yet its efects on developers with visual impairments remain largely unexplored. To address this gap, we used an Activity Theory framework to examine how developers with visual impairments interact with AI coding assistants. For this purpose, we conducted a study where developers who are visually impaired completed a series of programming tasks using a generative AI coding assistant. We uncovered that, while participants found the AI assistant benefcial and reported signifcant advantages, they also highlighted accessibility challenges. Specifcally, the AI coding assistant often exacerbated existing accessibility barriers and introduced new challenges. For example, it overwhelmed users with an excessive number of suggestions, leading developers who are visually impaired to express a desire for “AI timeouts.” Additionally, the generative AI coding assistant made it more difcult for developers to switch contexts between the AI-generated content and their own code. Despite these challenges, participants were optimistic about the potential of AI coding assistants to transform the coding experience for developers with visual impairments. Our fndings emphasize the need to apply activity-centered design principles to generative AI assistants, ensuring they better align with user behaviors and address specifc accessibility needs. This approach can enable the assistants to provide more intuitive, inclusive, and efective experiences, while also contributing to the broader goal of enhancing accessibility in software development 
    more » « less
  2. Open source software is commonly portrayed as a meritocracy, where decisions are based solely on their technical merit. However, literature on open source suggests a complex social structure underlying the meritocracy. Social work environments such as GitHub make the relationships between users and between users and work artifacts transparent. This transparency enables developers to better use information such as technical value and social connections when making work decisions. We present a study on open source software contribution in GitHub that focuses on the task of evaluating pull requests, which are one of the primary methods for contributing code in GitHub. We analyzed the association of various technical and social measures with the likelihood of contribution acceptance. We found that project managers made use of information signaling both good technical contribution practices for a pull request and the strength of the social connection between the submitter and project manager when evaluating pull requests. Pull requests with many comments were much less likely to be accepted, moderated by the submitter's prior interaction in the project. Well-established projects were more conservative in accepting pull requests. These findings provide evidence that developers use both technical and social information when evaluating potential contributions to open source software projects 
    more » « less
  3. Scholars have investigated numerous barriers to accessible software development tools and processes for Blind and Low Vision (BLV) developers. However, the research community has yet to study the accessibility of software development meetings, which are known to play a crucial role in software development practice. We conducted semi-structured interviews with 26 BLV software professionals about software development meeting accessibility. We found four key themes related to in-person and remote software development meetings: (1) participants observed that certain meeting activities and software tools used in meetings were inaccessible, (2) participants performed additional labor in order to make meetings accessible, (3) participants avoided disclosing their disability during meetings due to fear of career repercussions, (4) participants suggested technical, social and organizational solutions for accessible meetings, including developing their own solutions. We suggest recommendations and design implications for future accessible software development meetings including technical and policy-driven solutions. 
    more » « less
  4. Abstract Developing sustainable software for the scientific community requires expertise in software engineering and domain science. This can be challenging due to the unique needs of scientific software, the insufficient resources for software engineering practices in the scientific community, and the complexity of developing for evolving scientific contexts. While open‐source software can partially address these concerns, it can introduce complicating dependencies and delay development. These issues can be reduced if scientists and software developers collaborate. We present a case study wherein scientists from the SuperNova Early Warning System collaborated with software developers from the Scalable Cyberinfrastructure for Multi‐Messenger Astrophysics project. The collaboration addressed the difficulties of open‐source software development, but presented additional risks to each team. For the scientists, there was a concern of relying on external systems and lacking control in the development process. For the developers, there was a risk in supporting a user‐group while maintaining core development. These issues were mitigated by creating a second Agile Scrum framework in parallel with the developers' ongoing Agile Scrum process. This Agile collaboration promoted communication, ensured that the scientists had an active role in development, and allowed the developers to evaluate and implement the scientists' software requirements. The collaboration provided benefits for each group: the scientists actuated their development by using an existing platform, and the developers utilized the scientists' use‐case to improve their systems. This case study suggests that scientists and software developers can avoid scientific computing issues by collaborating and that Agile Scrum methods can address emergent concerns. 
    more » « less
  5. null (Ed.)
    Virtual conversational assistants designed specifically for software engineers could have a huge impact on the time it takes for software engineers to get help. Research efforts are focusing on virtual assistants that support specific software development tasks such as bug repair and pair programming. In this paper, we study the use of online chat platforms as a resource towards collecting developer opinions that could potentially help in building opinion Q&A systems, as a specialized instance of virtual assistants and chatbots for software engineers. Opinion Q&A has a stronger presence in chats than in other developer communications, thus mining them can provide a valuable resource for developers in quickly getting insight about a specific development topic (e.g., What is the best Java library for parsing JSON?). We address the problem of opinion Q&A extraction by developing automatic identification of opinion-asking questions and extraction of participants’ answers from public online developer chats. We evaluate our automatic approaches on chats spanning six programming communities and two platforms. Our results show that a heuristic approach to opinion-asking questions works well (.87 precision), and a deep learning approach customized to the software domain outperforms heuristics-based, machine-learning-based and deep learning for answer extraction in community question answering. 
    more » « less