The Software Foundations: mathematical underpinnings of reliable software(softwarefoundations.cis.upenn.edu)
softwarefoundations.cis.upenn.edu
The Software Foundations: mathematical underpinnings of reliable software
https://softwarefoundations.cis.upenn.edu/
26 comments
More specifically, Coq is based on the calculus of inductive constructions: https://en.m.wikipedia.org/wiki/Calculus_of_constructions.
The key differentiating feature being dependent types, whereas Isabelle/HOL implements higher-order logic without dependent types.
The key differentiating feature being dependent types, whereas Isabelle/HOL implements higher-order logic without dependent types.
Also check out Philip Wadler's Programming Language Foundations in Agda: https://plfa.github.io/
These books are surprisingly satisfying and fun to work through. The instant feedback from the proof checker makes them feel like a game of logic puzzles.
There’s another book, Concrete Semantics, that starts off by saying something along the lines of:
“Be careful - interactive theorem proving is addicting.”
It’s so true. You can end up ‘accidentally’ proving things, and when the proof checker accepts the proof it’s a big endorphin rush.
http://concrete-semantics.org/
“Be careful - interactive theorem proving is addicting.”
It’s so true. You can end up ‘accidentally’ proving things, and when the proof checker accepts the proof it’s a big endorphin rush.
http://concrete-semantics.org/
There is this story by the famous physicist Steven Wolfram who asked the infamous mathematician Grigori Perelman who proved the Poincare conjecture and was awarded, and subsequently declined, both the millennium price and field medal, what axiom set he used in proving the Poincare conjecture, to which Perelman answered, I don't know and I don't care.
[deleted]
Do you have any sources on that? I can not find anything about those interacting or Perelman saying that he does not care about the axioms of his work.
Recent Podcast by with Wolfram, maybe the quote is apocryphal or it was by another mathematician, anyway the point was that there is this "toxic" culture of always focusing on formal correct systems while not appreciating the creativity required todo these things. I remembers at some point in the proof of the Poincare conjecture Perelman uses big O notation to argue that one concept is related to another, using a concept from analysis that everyone know in a novel way to proof something new.
Amazing, was literally just thinking about how this is one area I've always been interested in but never taken the leap
Has anything actually useful ever come out of this field of enquiry? To me it always seems like excessive formalism for its own sake without a useful real-world outcome. Would be happy to be wrong about this.
Apart from the intellectual clarity, you don't need to employ all of the tools in this text to benefit practically from some use of formal verification, etc. If you're using a statically typed language, you're likely already benefiting from at least some degree of verification. Your types encode your specification.
One example close to home for me and from industry is a dependently typed language we are working on at my company that's used to encode validations and transformations for transaction reporting (other teams have also begun to use the language for other uses). Consistency is ensured by the type checker and the compiler subsequently generates the aforementioned transformation and validation functions that are used in production. This is admittedly a very niche application, but as I've already written, the use of static analysis admits a range of rigor—it's not either/or—so it's a question of determining the appropriate degree of formality for your particular case.
One example close to home for me and from industry is a dependently typed language we are working on at my company that's used to encode validations and transformations for transaction reporting (other teams have also begun to use the language for other uses). Consistency is ensured by the type checker and the compiler subsequently generates the aforementioned transformation and validation functions that are used in production. This is admittedly a very niche application, but as I've already written, the use of static analysis admits a range of rigor—it's not either/or—so it's a question of determining the appropriate degree of formality for your particular case.
Yes! Formally verified implementations of Elliptic Curve algorithms http://adam.chlipala.net/theses/andreser_meng.pdf. Amazon has also made use of TLA+ and lightweight formal methods to prove the correctness of their distributed services such as S3 and DynamoDB which arguably underpin a large portion of the internet https://www.amazon.science/publications/how-amazon-web-servi...
The burden of using these extreme approaches is high, but there are definitely circumstances where it is warranted. Think of it as TDD on steroids.
The burden of using these extreme approaches is high, but there are definitely circumstances where it is warranted. Think of it as TDD on steroids.
The seL4 microkernel: https://sel4.systems/
The CompCert C compiler: https://compcert.org/
TLS implementation in Firefox: https://blog.mozilla.org/security/2020/07/06/performance-imp...
Elasticsearch model checks some of their core algorithms with TLA+: https://youtu.be/qYDcbcOVurc.
Amazon is known to apply formal methods in varying forms to services like S3: https://www.amazon.science/publications/using-lightweight-fo...
Many components in airplane software is formally verified in some aspect.
The CompCert C compiler: https://compcert.org/
TLS implementation in Firefox: https://blog.mozilla.org/security/2020/07/06/performance-imp...
Elasticsearch model checks some of their core algorithms with TLA+: https://youtu.be/qYDcbcOVurc.
Amazon is known to apply formal methods in varying forms to services like S3: https://www.amazon.science/publications/using-lightweight-fo...
Many components in airplane software is formally verified in some aspect.
Not an expert but I've heard formal methods are used in Chip Design. Also https://compcert.org/ a c compiler which uses formal verifcation. I tried some exercises in the series. Its pretty interesting thing to do (but very difficult to master), but yes I don't think its great for rapid software development. On the other hand for very very critical infrastructure or the case where you need your code to be right from the start (chip design, security protocols, etc.) it makes sense.
What do you mean by field of enquiry?
Formal verification has it's success stories, like seL4 (https://sel4.systems/).
This series seems rather educational and seems to give you coq proofs for algorithms. I guess it depends on your needs and domain if you need to bother.
Formal verification has it's success stories, like seL4 (https://sel4.systems/).
This series seems rather educational and seems to give you coq proofs for algorithms. I guess it depends on your needs and domain if you need to bother.
The Rust borrow checker implements what amounts to a simplified application of separation logic (the topic of the latest volume in this series), and there's ongoing work to further extend its applicability so that, e.g. generic data structure implementations might be written in a verifiably safe manner. If you've ever written or otherwise relied on Rust software, you have indirectly used this work.
As far as I know, formal methods are used in system design.
AWS build some of it's services with their help.
AWS build some of it's services with their help.
too hard to read though. Couldn't identify it as "foundation"
It's talking about idealistic foundations. The idea that software being a theoretical language with a well defined domain and codomain can be written with zero bugs and zero testing to catch those bugs. Zero bug code is written utilizing the tools of math, such as axioms, theorems, and logic to derive zero bug code without the need to utilize engineering principles. (I'm exaggerating a bit with the word "zero", "nearly zero" is more accurate, but too wordy)
In practice we try to eliminate bugs in software engineering by doing testing as if software was some material with unknown properties. This method is easy to understand but ultimately has it's weaknesses as tests only prove a program works for a single test. This is the "foundation" most engineers are use to.
As I stated previously, the "foundation" these book refer to are an idealism involving proving an entire program to be bug free without running it or testing it. Hence this is the reason why it's so foreign to you. You're likely use to software from a testing perspective.
Vestiges of this "foundation" have leaked into the common practice of software engineering. It's called type checking. In type checking your computer uses a similar method to guarantee your program has zero type bugs. It doesn't run any type testing, it literally just proves that your program is type safe and correct.
In practice we try to eliminate bugs in software engineering by doing testing as if software was some material with unknown properties. This method is easy to understand but ultimately has it's weaknesses as tests only prove a program works for a single test. This is the "foundation" most engineers are use to.
As I stated previously, the "foundation" these book refer to are an idealism involving proving an entire program to be bug free without running it or testing it. Hence this is the reason why it's so foreign to you. You're likely use to software from a testing perspective.
Vestiges of this "foundation" have leaked into the common practice of software engineering. It's called type checking. In type checking your computer uses a similar method to guarantee your program has zero type bugs. It doesn't run any type testing, it literally just proves that your program is type safe and correct.
Thank you for this comment, you shed some light on something I considered too opaque to dig into and made it clear why this would be useful.
> as if software was some material with unknown properties
That‘s a great way to put it!
That‘s a great way to put it!
Addition is something you learn in elementary school. Building the set of integers is taught in university.
Just because something is a foundation, doesn't mean it's easier to understand than the things build upon it.
Just because something is a foundation, doesn't mean it's easier to understand than the things build upon it.
I'm probably not the best person to say what I'm about to say.
In my university days, I took a graduate-level class called Software Foundations.
We used Haskell to learn and implement type systems and a few other things.
At the time I had no idea why it has "foundation" in the course title, because to me all of that was advanced stuff.
Eventually, I had my moment of enlightenment, and it all became clear to me. These where infact theoretical underpinnings of software.
Till then, I've only seen computation from the perspective of electricity->bits->circuits->...->assembly->the C language (and everything that comes above it).
Over there, the "foundation" was bits and electronics using which you can make logic gates, develop the arithmetic & logic unit (ALU) and control unit, and build everything on top.
On the other hand, with Lambda calculus, Church numerals etc I was approaching computation from the other direction — the mathematical perspective. It's also foundational, in that you can build up everything that you need — ALU and control unit — using Lambda calculus.
Indeed it was eerie the first time I added on paper two Church numerals using Lamba calculus and the correct result popped out. Even though I knew the theory was sound — and I know this is a dumb thing to say — it was still so cool to see it work in practice.
In my university days, I took a graduate-level class called Software Foundations.
We used Haskell to learn and implement type systems and a few other things.
At the time I had no idea why it has "foundation" in the course title, because to me all of that was advanced stuff.
Eventually, I had my moment of enlightenment, and it all became clear to me. These where infact theoretical underpinnings of software.
Till then, I've only seen computation from the perspective of electricity->bits->circuits->...->assembly->the C language (and everything that comes above it).
Over there, the "foundation" was bits and electronics using which you can make logic gates, develop the arithmetic & logic unit (ALU) and control unit, and build everything on top.
On the other hand, with Lambda calculus, Church numerals etc I was approaching computation from the other direction — the mathematical perspective. It's also foundational, in that you can build up everything that you need — ALU and control unit — using Lambda calculus.
Indeed it was eerie the first time I added on paper two Church numerals using Lamba calculus and the correct result popped out. Even though I knew the theory was sound — and I know this is a dumb thing to say — it was still so cool to see it work in practice.
yeah it is a hard read. a relatively easier read is PLFA in Agda.
This relies on the Coq proof assistant. From what I've begun to understand, they use 'higher order logic', which really means they can quantify (for all, there exists) over things with cardinalities larger than the countably infinite.