Document Open Access Logo

The End of History? Using a Proof Assistant to Replace Language Design with Library Design

Authors Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang, Katherine Ye

PDF
Thumbnail PDF

File

LIPIcs.SNAPL.2017.3.pdf
  • Filesize: 0.52 MB
  • 15 pages

Document Identifiers

Author Details

Adam Chlipala
Benjamin Delaware
Samuel Duchovni
Jason Gross
Clément Pit-Claudel
Sorawit Suriyakarn
Peng Wang
Katherine Ye

Cite As Get BibTex

Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang, and Katherine Ye. The End of History? Using a Proof Assistant to Replace Language Design with Library Design. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 3:1-3:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.SNAPL.2017.3

Abstract

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.

Subject Classification

Keywords
  • Domain-specific languages
  • synthesis
  • verification
  • proof assistants
  • software development

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. David R. Barstow. Domain-specific automatic programming. IEEE Softw., 11(11):1321-1336, November 1985. URL: http://dx.doi.org/10.1109/TSE.1985.231881.
  2. Jon Bentley. Programming pearls: Little languages. Commun. ACM, 29(8):711-721, August 1986. URL: http://dx.doi.org/10.1145/6424.315691.
  3. Lee Blaine and Allen Goldberg. DTRE - a semi-automatic transformation system. In Constructing Programs from Specifications, pages 165-204. Elsevier, 1991. Google Scholar
  4. Aaron Bohannon, J. Nathan Foster, Benjamin C. Pierce, Alexandre Pilkiewicz, and Alan Schmitt. Boomerang: resourceful lenses for string data. In Proc. POPL, pages 407-419, 2008. URL: http://dx.doi.org/10.1145/1328438.1328487.
  5. Adam Chlipala. The Bedrock structured programming system: Combining generative metaprogramming and Hoare logic in an extensible program verifier. In Proc. ICFP. Association for Computing Machinery (ACM), 2013. URL: http://dx.doi.org/10.1145/2500365.2500592.
  6. Cyril Cohen, Maxime Dénès, and Anders Mörtberg. Refinements for free! Lecture Notes in Computer Science, pages 147-162, 2013. URL: http://dx.doi.org/10.1007/978-3-319-03545-1_10.
  7. Benjamin Delaware, Clément Pit-Claudel, Jason Gross, and Adam Chlipala. Fiat: Deductive synthesis of abstract data types in a proof assistant. In Proc. POPL, pages 689-700. Association for Computing Machinery (ACM), 2015. URL: http://dx.doi.org/10.1145/2676726.2677006.
  8. Edsger W. Dijkstra. A constructive approach to the problem of program correctness. Circulated privately, August 1967. URL: http://www.cs.utexas.edu/users/EWD/ewd02xx/EWD209.PDF.
  9. Sebastian Egner, Jeremy Johnson, David Padua, Jianxin Xiong, and Markus Püschel. Automatic derivation and implementation of signal processing algorithms. SIGSAM Bull., 35(2):1-19, June 2001. URL: http://dx.doi.org/10.1145/511988.511990.
  10. Georges Gonthier. Formal proof - the four-color theorem. Not. ACM, 55(11):1382-1393, 2008. Google Scholar
  11. Jason Gross. An extensible framework for synthesizing efficient, verified parsers. Master’s thesis, Massachusetts Institute of Technology, September 2015. URL: https://people.csail.mit.edu/jgross/personal-website/papers/2015-jgross-thesis.pdf, URL: http://dx.doi.org/1721.1/101581.
  12. Michael Hammer. The design of usable programming languages. In Proc. ACM, ACM'75, pages 225-229, New York, NY, USA, 1975. ACM. URL: http://dx.doi.org/10.1145/800181.810327.
  13. Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin Rinard, and Mooly Sagiv. Data representation synthesis. In Proc. PLDI, PLDI'11, pages 38-49, New York, NY, USA, 2011. ACM. URL: http://dx.doi.org/10.1145/1993498.1993504.
  14. J. He, C. A. R. Hoare, and J. W. Sanders. Data refinement refined. In Proc. ESOP, volume 213, pages 187-196. Springer Berlin Heidelberg, 1986. URL: http://dx.doi.org/10.1007/3-540-16442-1_14.
  15. C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4):271-281, 1972. URL: http://dx.doi.org/10.1007/BF00289507.
  16. E. Horowitz, A. Kemper, and B. Narasimhan. A survey of application generators. IEEE Softw., 2(1):40-54, January 1985. URL: http://dx.doi.org/10.1109/MS.1985.230048.
  17. Shachar Itzhaky, Rohit Singh, Armando Solar-Lezama, Kuat Yessenov, Yongquan Lu, Charles Leiserson, and Rezaul Chowdhury. Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations. In Proc. OOPSLA. Association for Computing Machinery (ACM), 2016. URL: http://dx.doi.org/10.1145/2983990.2983993.
  18. Lennart C.L. Kats and Eelco Visser. The Spoofax language workbench: Rules for declarative specification of languages and IDEs. In Proc. OOPSLA, OOPSLA'10, pages 444-463, New York, NY, USA, 2010. ACM. URL: http://dx.doi.org/10.1145/1869459.1869497.
  19. Etienne Kneuss, Ivan Kuraj, Viktor Kuncak, and Philippe Suter. Synthesis modulo recursive functions. In Proc. OOPSLA, pages 407-426, 2013. URL: http://dx.doi.org/10.1145/2509136.2509555.
  20. Donald E. Knuth. Structured programming with go to statements. ACM Comput. Surv., 6(4):261-301, December 1974. URL: http://dx.doi.org/10.1145/356635.356640.
  21. Peter Lammich. Refinement to Imperative/HOL. In Proc. ITP, volume 9236 of Lecture Notes in Computer Science, pages 253-269. Springer International Publishing, 2015. URL: http://dx.doi.org/10.1007/978-3-319-22102-1_17.
  22. Peter Lammich and Thomas Tuerk. Applying data refinement for monadic programs to Hopcroft’s algorithm. In Lennart Beringer and Amy Felty, editors, Proc. ITP, volume 7406 of Lecture Notes in Computer Science, pages 166-182. Springer Berlin Heidelberg, 2012. URL: http://dx.doi.org/10.1007/978-3-642-32347-8_12.
  23. Daan Leijen and Erik Meijer. Domain specific embedded compilers. In Proc. DSL, pages 109-122, 1999. URL: http://dx.doi.org/10.1145/331960.331977.
  24. K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In Proc. LPAR, pages 348-370, 2010. URL: http://dx.doi.org/10.1007/978-3-642-17511-4_20.
  25. K. Rustan M. Leino and Aleksandar Milicevic. Program extrapolation with Jennisys. In Proc. OOPSLA, pages 411-430, 2012. URL: http://dx.doi.org/10.1145/2384616.2384646.
  26. Xavier Leroy. Formal certification of a compiler back-end or: Programming a compiler with a proof assistant. In Proc. POPL, pages 42-54. Association for Computing Machinery (ACM), 2006. URL: http://dx.doi.org/10.1145/1111037.1111042.
  27. Barbara Liskov and Stephen Zilles. Programming with abstract data types. In Proc. VHLL, pages 50-59, New York, NY, USA, 1974. ACM. URL: http://dx.doi.org/10.1145/800233.807045.
  28. Calvin Loncaric, Emina Torlak, and Michael D. Ernst. Fast synthesis of fast collections. In Proc. PLDI, pages 355-368, 2016. URL: http://dx.doi.org/10.1145/2908080.2908122.
  29. H. Partsch and R. Steinbrüggen. Program transformation systems. ACM Comput. Surv., 15(3):199-236, September 1983. URL: http://dx.doi.org/10.1145/356914.356917.
  30. Dusko Pavlovic, Peter Pepper, and Douglas R. Smith. Formal derivation of concurrent garbage collectors. In Proc. MPC, pages 353-376, 2010. URL: http://dx.doi.org/10.1007/978-3-642-13321-3_20.
  31. Clément Pit-Claudel. Compilation using correct-by-construction program synthesis. Master’s thesis, Massachusetts Institute of Technology, August 2016. URL: http://pit-claudel.fr/clement/MSc/, URL: http://dx.doi.org/1721.1/107293.
  32. Tiark Rompf, Arvind K. Sujeeth, Nada Amin, Kevin J. Brown, Vojin Jovanovic, HyoukJoong Lee, Manohar Jonnalagedda, Kunle Olukotun, and Martin Odersky. Optimizing data structures in high-level programs: New directions for extensible compilers based on staging. In Proc. POPL, POPL'13, pages 497-510, New York, NY, USA, 2013. ACM. URL: http://dx.doi.org/10.1145/2429069.2429128.
  33. Edmond Schonberg, Jacob T. Schwartz, and Micha Sharir. Automatic data structure selection in SETL. In Proc. POPL. Association for Computing Machinery (ACM), 1979. URL: http://dx.doi.org/10.1145/567752.567771.
  34. Douglas R. Smith. KIDS: A semiautomatic program development system. IEEE Softw., 16(9):1024-1043, September 1990. URL: http://dx.doi.org/10.1109/32.58788.
  35. Douglas R. Smith and Stephen J. Westfold. Synthesis of propositional satisfiability solvers. Manuscript, 2008. Google Scholar
  36. Armando Solar-Lezama, Rodric Rabbah, Rastislav Bodík, and Kemal Ebcioğlu. Programming by sketching for bit-streaming programs. In Proc. PLDI, PLDI'05, pages 281-294, New York, NY, USA, 2005. ACM. URL: http://dx.doi.org/10.1145/1065010.1065045.
  37. Specware. URL: http://www.kestrel.edu/home/prototypes/specware.html.
  38. Sam Tobin-Hochstadt, Vincent St-Amour, Ryan Culpepper, Matthew Flatt, and Matthias Felleisen. Languages as libraries. In Proc. PLDI, PLDI'11, pages 132-141, New York, NY, USA, 2011. ACM. URL: http://dx.doi.org/10.1145/1993498.1993514.
  39. Tijs van der Storm, William R. Cook, and Alex Loh. Object grammars: Compositional and bidirectional mapping between text and graphs. In Proc. SLE, pages 4-23, 2012. URL: http://dx.doi.org/10.1007/978-3-642-36089-3_2.
  40. Arie van Deursen, Paul Klint, and Joost Visser. Domain-specific languages: An annotated bibliography. SIGPLAN Not., 35(6):26-36, June 2000. URL: http://dx.doi.org/10.1145/352029.352035.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact