The Software Foundations: mathematical underpinnings of reliable software

I&#x27;m taking a formal verification course about this right now using the logical foundations volume.<p>This relies on the Coq proof assistant. From what I&#x27;ve begun to understand, they use &#x27;higher order logic&#x27;, which really means they can quantify (for all, there exists) over things with cardinalities larger than the countably infinite.

Also check out Philip Wadler&#x27;s Programming Language Foundations in Agda: <a href="https:&#x2F;&#x2F;plfa.github.io&#x2F;" rel="nofollow">https:&#x2F;&#x2F;plfa.github.io&#x2F;</a>

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 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&#x27;t know and I don&#x27;t care.

Amazing, was literally just thinking about how this is one area I&#x27;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.

too hard to read though. Couldn&#x27;t identify it as &quot;foundation&quot;