[Pl-seminar] Seminar tomorrow: Gwenyth Lincroft on Proof Assistant Ecosystems

[Luna Phipps-Costin]

Hi all -

Tomorrow at our PL seminar, Gwen will be presenting what will double as 
an ICSE practice talk.

Where:   WVH 366

When:   Tomorrow Apr 9, 12:30-1:30. Lunch will be served 12-12:30

Speaker:   Gwenyth Lincroft

Title:    Thirty-Three Years of Mathematicians and Software Engineers: A 
Case Study of Domain Expertise and Participation in Proof Assistant 
Ecosystems

Abstract:   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.