The Programatica Project
Integrating Programming, Properties and Validation

Introduction

The goals of the Programatica project were to

• develop methodologies, tools and foundations to support the construction and certification of high-assurance systems.
• integrate a broad and open spectrum of assurance techniques (code review, testing, formal methods, ...)
• support evolving code, evidence, and assurance requirements (e.g., track dependencies, revalidate evidence, ...)
• apply to assurance of security properties in complex software artifacts of engineering significance.

The Programatica approach to achieving these goals was to

• build a program development environment that supports and encourages its users in thinking about, stating, and validating key properties.
• enable programming and validation to proceed hand in hand, using properties to link the two.
• allow users to realize benefits gradually by choosing between varying levels of assurance.

The key components used were

• a semantically rich, formal modeling and implementation language (Haskell).
• an expressive programming logic that can be used to capture critical program properties (P-logic). [TODO: Link to a nice introduction to P-logic]
• a toolset for creating, maintaining, and auditing the supporting evidence (pfe, cert, ...).

[TODO: say something about Osker and House]