by bsedlm on 3/5/22, 2:51 PM
I'm taking a formal verification course about this right now using the logical foundations volume.
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.
by dennis_moore on 3/5/22, 7:55 PM
by bombastry on 3/5/22, 5:09 PM
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.
by wrnr on 3/5/22, 1:00 PM
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.
by jackosdev on 3/5/22, 10:32 AM
Amazing, was literally just thinking about how this is one area I've always been interested in but never taken the leap
by caffeine on 3/5/22, 11:11 AM
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.
by lobstey on 3/5/22, 8:04 AM
too hard to read though. Couldn't identify it as "foundation"