Archive for the ‘Dependency’ Category

Verified Networking using Dependent Types

Sunday, May 25th, 2014

Verified Networking using Dependent Types by Simon Fowler.

Abstract:

Strongly, statically typed functional programming languages have found a strong grounding in academia and industry for a variety of reasons: they are concise, their type systems provide additional static correctness guarantees, and the structured management of side effects aids easier reasoning about the operation of programs, to name but a few.

Dependently-typed languages take these concepts a step further: by allowing types to be predicated on values, it is possible to impose arbitrarily specific type constraints on functions, resulting in increased confidence about their runtime behaviour.

This work demonstrates how dependent types may be used to increase confidence in network applications. We show how dependent types may be used to enforce resource usage protocols inherent in C socket programming, providing safety guarantees, and examine how a dependently- typed embedded domain-specific language may be used to enforce the conformance of packets to a given structure. These concepts are explored using two larger case studies: packets within the Domain Name System (DNS) and a networked game.

The use of statically typed functional programming languages is spreading. Fowler’s dissertation is yet another illustration of that fact.

When you read:

…examine how a dependently- typed embedded domain-specific language may be used to enforce the conformance of packets to a given structure.

Do you also hear:

…examine how a dependently- typed embedded domain-specific language may be used to enforce the conformance of proxies to a given structure.

??

Certified Programming with Dependent Types

Thursday, January 30th, 2014

Certified Programming with Dependent Types by Adam Chlipala.

From the introduction:

We would all like to have programs check that our programs are correct. Due in no small part to some bold but unfulfilled promises in the history of computer science, today most people who write software, practitioners and academics alike, assume that the costs of formal program verification outweigh the benefits. The purpose of this book is to convince you that the technology of program verification is mature enough today that it makes sense to use it in a support role in many kinds of research projects in computer science. Beyond the convincing, I also want to provide a handbook on practical engineering of certified programs with the Coq proof assistant. Almost every subject covered is also relevant to interactive computer theorem-proving in general, such as for traditional mathematical theorems. In fact, I hope to demonstrate how verified programs are useful as building blocks in all sorts of formalizations.

The idea of certified program features prominently in this book’s title. Here the word “certified” does not refer to governmental rules for how the reliability of engineered systems may be demonstrated to sufficiently high standards. Rather, this concept of certification, a standard one in the programming languages and formal methods communities, has to do with the idea of a certificate, or formal mathematical artifact proving that a program meets its specification. Government certification procedures rarely provide strong mathematical guarantees, while certified programming provides guarantees about as strong as anything we could hope for. We trust the definition of a foundational mathematical logic, we trust an implementation of that logic, and we trust that we have encoded our informal intent properly in formal specifications, but few other opportunities remain to certify incorrect software. For compilers and other programs that run in batch mode, the notion of a certifying program is also common, where each run of the program outputs both an answer and a proof that the answer is correct. Any certifying program can be composed with a proof checker to produce a certified program, and this book focuses on the certified case, while also introducing principles and techniques of general interest for stating and proving theorems in Coq.

It is hard to say whether this effort at certified programming will prove to be any more successful than Z notation.

On the other hand, the demand for programs that are provably free of government intrusion or backdoors, is at an all time high.

Government overreaching, overreaching that was disproportionate to any rational goal, will power the success of open source programming and the advent of certified programs.

Ironic that such a pernicious activity will have such unintended good results.

I first saw this in a tweet by Computer Science.

Development at the Speed and Scale of Google

Friday, September 16th, 2011

Development at the Speed and Scale of Google by Ashish Kumar.

Interesting overview of development at Google. I included it as a background for the question:

How would you use topic maps as part of documenting a development process?

Or perhaps better: Are you using topic maps as part of a development process and if so, how?

Now that I think about it, there may be another way to approach the use of topic map in software engineering. Harvest the bug reports and push those through text processing tools. I haven’t ever thought of bug reports as a genre but I suspect it has all the earmarks of one.

Thoughts? Comments?