The end of history? Using a proof assistant to replace language design with library design
Functionality of software systems has exploded in part because of advances in programming language support for packaging reusable functionality as libraries. Developers benefit from the uniformity that comes of exposing many interfaces in the same language, as opposed to stringing together hodgepodg...
| Main Authors: | , , , , , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | English |
| Published: |
Dagstuhl Research
2020
|
| Online Access: | https://hdl.handle.net/1721.1/128880 |
| _version_ | 1826205074039242752 |
|---|---|
| author | Chlipala, Adam Delaware, Benjamin Duchovni, Samuel Gross, Jason S. Pit-Claudel, Clement Francois Suriyakarn, Sorawit Wang, Peng |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Chlipala, Adam Delaware, Benjamin Duchovni, Samuel Gross, Jason S. Pit-Claudel, Clement Francois Suriyakarn, Sorawit Wang, Peng |
| author_sort | Chlipala, Adam |
| collection | MIT |
| description | Functionality of software systems has exploded in part because of advances in programming language support for packaging reusable functionality as libraries. Developers benefit from the uniformity that comes of exposing many interfaces in the same language, as opposed to stringing together hodgepodges of command-line tools. Domain-specific languages may be viewed as an evolution of the power of reusable interfaces, when those interfaces become so flexible as to deserve to be called programming languages. However, common approaches to domain-specific languages give up many of the hard-won advantages of library-building in a rich common language, and even the traditional approach poses significant challenges in learning new APIs. We suggest that instead of continuing to develop new domain-specific languages, our community should embrace library-based ecosystems within very expressive languages that mix programming and theorem proving. Our prototype framework Fiat, a library for the Coq proof assistant, turns languages into easily comprehensible libraries via the key idea of modularizing functionality and performance away from each other, the former via macros that desugar into higher-order logic and the latter via optimization scripts that derive efficient code from logical programs. |
| first_indexed | 2024-09-23T13:06:19Z |
| format | Article |
| id | mit-1721.1/128880 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2024-09-23T13:06:19Z |
| publishDate | 2020 |
| publisher | Dagstuhl Research |
| record_format | dspace |
| spelling | mit-1721.1/1288802021-09-10T19:27:24Z The end of history? Using a proof assistant to replace language design with library design Chlipala, Adam Delaware, Benjamin Duchovni, Samuel Gross, Jason S. Pit-Claudel, Clement Francois Suriyakarn, Sorawit Wang, Peng Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Functionality of software systems has exploded in part because of advances in programming language support for packaging reusable functionality as libraries. Developers benefit from the uniformity that comes of exposing many interfaces in the same language, as opposed to stringing together hodgepodges of command-line tools. Domain-specific languages may be viewed as an evolution of the power of reusable interfaces, when those interfaces become so flexible as to deserve to be called programming languages. However, common approaches to domain-specific languages give up many of the hard-won advantages of library-building in a rich common language, and even the traditional approach poses significant challenges in learning new APIs. We suggest that instead of continuing to develop new domain-specific languages, our community should embrace library-based ecosystems within very expressive languages that mix programming and theorem proving. Our prototype framework Fiat, a library for the Coq proof assistant, turns languages into easily comprehensible libraries via the key idea of modularizing functionality and performance away from each other, the former via macros that desugar into higher-order logic and the latter via optimization scripts that derive efficient code from logical programs. NSF (Grants CCF-1253229, CCF-1512611 and CCF-1521584) DARPA (Contracts FA8750-12-2-0293 and FA8750-16-C-0007) 2020-12-21T20:37:27Z 2020-12-21T20:37:27Z 2017-05 2017-03 2019-05-13T17:46:41Z Article http://purl.org/eprint/type/ConferencePaper https://hdl.handle.net/1721.1/128880 Chlipala, Adam et al. "The end of history? Using a proof assistant to replace language design with library design." 2nd Summit on Advances in Programming Languages, May 2017, Asilomar, California, Dagstuhl Research, May 2017. © 2017 The Authors en http://dx.doi.org/10.4230/LIPIcs.SNAPL.2017.3 2nd Summit on Advances in Programming Languages Creative Commons Attribution 4.0 International license http://creativecommons.org/licenses/by-nc-nd/4.0/ application/pdf Dagstuhl Research DROPS |
| spellingShingle | Chlipala, Adam Delaware, Benjamin Duchovni, Samuel Gross, Jason S. Pit-Claudel, Clement Francois Suriyakarn, Sorawit Wang, Peng The end of history? Using a proof assistant to replace language design with library design |
| title | The end of history? Using a proof assistant to replace language design with library design |
| title_full | The end of history? Using a proof assistant to replace language design with library design |
| title_fullStr | The end of history? Using a proof assistant to replace language design with library design |
| title_full_unstemmed | The end of history? Using a proof assistant to replace language design with library design |
| title_short | The end of history? Using a proof assistant to replace language design with library design |
| title_sort | end of history using a proof assistant to replace language design with library design |
| url | https://hdl.handle.net/1721.1/128880 |
| work_keys_str_mv | AT chlipalaadam theendofhistoryusingaproofassistanttoreplacelanguagedesignwithlibrarydesign AT delawarebenjamin theendofhistoryusingaproofassistanttoreplacelanguagedesignwithlibrarydesign AT duchovnisamuel theendofhistoryusingaproofassistanttoreplacelanguagedesignwithlibrarydesign AT grossjasons theendofhistoryusingaproofassistanttoreplacelanguagedesignwithlibrarydesign AT pitclaudelclementfrancois theendofhistoryusingaproofassistanttoreplacelanguagedesignwithlibrarydesign AT suriyakarnsorawit theendofhistoryusingaproofassistanttoreplacelanguagedesignwithlibrarydesign AT wangpeng theendofhistoryusingaproofassistanttoreplacelanguagedesignwithlibrarydesign AT chlipalaadam endofhistoryusingaproofassistanttoreplacelanguagedesignwithlibrarydesign AT delawarebenjamin endofhistoryusingaproofassistanttoreplacelanguagedesignwithlibrarydesign AT duchovnisamuel endofhistoryusingaproofassistanttoreplacelanguagedesignwithlibrarydesign AT grossjasons endofhistoryusingaproofassistanttoreplacelanguagedesignwithlibrarydesign AT pitclaudelclementfrancois endofhistoryusingaproofassistanttoreplacelanguagedesignwithlibrarydesign AT suriyakarnsorawit endofhistoryusingaproofassistanttoreplacelanguagedesignwithlibrarydesign AT wangpeng endofhistoryusingaproofassistanttoreplacelanguagedesignwithlibrarydesign |