Home

Ensuring Correct-by-Construction Resource Usage by using Full-Spectrum Dependent Types

Ensuring Correct-by-Construction Resource Usage by using Full-Spectrum Dependent Types

Where it has been done at all, formally demonstrating the correctness of functional programs has historically focused on proving essential properties derived from the functional specification of the software. In this paper, we show that correct-by-construction software development can also handle the equally important class of extra-functional properties, namely the correct usage of resources. We do this using a novel embedded domain-specific language approach that exploits the capabilities of full-spectrum dependent types. Our approach provides significant benefits over previous approaches based on less powerful type systems in reducing notational overhead, and in simplifying the process of formal proof.

More ammunition for the importance of embedded domain-specific languages, dependent types, and correctness-by-construction.

By Paul Snively at 2009-03-04 17:17 | DSL | Functional | Implementation | Type Theory | other blogs | 7649 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Importance

More ammunition for the importance of embedded domain-specific languages, dependent types, and correctness-by-construction.

I'd say that this is ammunition for the possibility of these things (except EDSLs, which are widespread). I'll believe in the importance when they're used in programs people use.

By Sam Tobin-Hochstadt at Thu, 2009-03-05 13:36 | login or register to post comments

The Importance...

...is to the creation of the increasingly-complex software that people will be willing to use in the future. Present popularity isn't a particularly good indicator of importance.

By Paul Snively at Thu, 2009-03-05 17:51 | login or register to post comments