TL;DR
Proof Driven Development is a novel software development workflow that extends test-driven development by incorporating dependently typed programming to enhance proof capabilities and software correctness.
Contribution
It introduces proof-driven development as an extension of test-driven development, leveraging dependently typed programming to improve software correctness and expressiveness.
Findings
Enhanced ability to express properties in proofs
Comparison of proof-driven and test-driven workflows
Discussion on complexity and provability in software design
Abstract
A new workflow for software development (proof-driven development) is presented. An extension of test-driven development, the new workflow utilizes the paradigm of dependently typed programming. The differences in design, complexity and provability of software are discussed, based on the technique used to create the system. Furthermore, the difference in what properties can be expressed in a proof-driven development workflow versus a traditional test-driven development workflow or using test-last development.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Advanced Software Engineering Methodologies · Software Engineering Research