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.
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 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.
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.
AWS build some of it's services with their help.
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.
That‘s a great way to put it!
Just because something is a foundation, doesn't mean it's easier to understand than the things build upon it.
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.
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.
The key differentiating feature being dependent types, whereas Isabelle/HOL implements higher-order logic without dependent types.
“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.
