References:
[Video Class, Benjamin C. Pierce]()
Building reliable software is really hard – really hard. The scale and complexity of modern systems, the number of people involved, and the range of demands placed on them make it challenging to build software that is even more-or-less correct, much less 100% correct. At the same time, the increasing degree to which information processing is woven into every aspect of society greatly amplifies the cost of bugs and insecurities.
Computer scientists and software engineers have responded to these challenges by developing a host of techniques for improving software reliability, ranging from recommendations about managing software project teams (e.g., extreme programming) to design philosophies for libraries (e.g., model-view-controller, publish-subscribe, etc.) and programming languages (e.g., object-oriented programming, aspect-oriented programming, functional programming, …) to mathematical techniques for specifying and reasoning about properties of software and tools for helping validate these properties. The Software Foundations series is focused on this last set of tools.
References: Software Foundations, Volume 1, Logical Foundations Video Class2, Micheal Ryan Clarkson [QED at large, Ringer et al., 2019]() Preface Source of Knowledge Source of Knowledge [Mechanizing Proof. MacKenzie 2001] Authority Inductive reasoning Deductive reasoning Inductive vs. Deductive cite: https://www.voxco.com/blog/inductive-vs-deductive-reasoning/ Inductive reasoning Inductive reasoning is a logical thinking process that integrates observations with experiential information to draw a conclusion. You are employing the use of inductive reasoning every time you
References: reference More
References: Software Foundations Volume 3, Verified Functional Algorithms, by Andrew W. Appel, with contributions from Andrew Tolmach and Micheal Clarkson. More
References: reference More
References: Verifiable C, version 2.11, 2022-08-19 Overview Verifiable C is a a language. The language is a subset of CompCert C light; it is a dialect of C in which side-effects and loads have been factored out of expressions. Verifiable C is a program logic. The program logic is a higher-order separation logic, a kind of Hoare logic with better support for reasoning about pointer data structures, function pointers, and data abstraction.
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?