armchair_progamer@programming.dev • 9 months agoI formally modeled Dreidel for no good reasonplus-squareexternal-linkmessage-square1 fedilinkarrow-up110
arrow-up110external-linkI formally modeled Dreidel for no good reasonplus-squarearmchair_progamer@programming.dev • 9 months agomessage-square1 Commentsfedilink
armchair_progamer@programming.dev • 9 months agoTLA+ in Isabelle/HOLplus-squareexternal-linkmessage-square0 fedilinkarrow-up14
arrow-up14external-linkTLA+ in Isabelle/HOLplus-squarearmchair_progamer@programming.dev • 9 months agomessage-square0 Commentsfedilink
armchair_progamer@programming.dev • 1 year agorzk: an experimental proof assistant for synthetic ∞-categoriesplus-squareexternal-linkmessage-square0 fedilinkarrow-up11
arrow-up11external-linkrzk: an experimental proof assistant for synthetic ∞-categoriesplus-squarearmchair_progamer@programming.dev • 1 year agomessage-square0 Commentsfedilink
armchair_progamer@programming.dev • 1 year agoLean/Coq/Isabel and Their Proof Treesplus-squareexternal-linkmessage-square0 fedilinkarrow-up11
arrow-up11external-linkLean/Coq/Isabel and Their Proof Treesplus-squarearmchair_progamer@programming.dev • 1 year agomessage-square0 Commentsfedilink
synthetic_apriori@programming.devM • 1 year agoSo you want to be a proof engineer?external-linkmessage-square0 fedilinkarrow-up11
arrow-up11external-linkSo you want to be a proof engineer?synthetic_apriori@programming.devM • 1 year agomessage-square0 Commentsfedilink
demesisx@programming.dev • 1 year ago#239 Grigore Rosu: The K framework - a framework to formally define all programming languagesplus-squareexternal-linkmessage-square0 fedilinkarrow-up11
arrow-up11external-link#239 Grigore Rosu: The K framework - a framework to formally define all programming languagesplus-squaredemesisx@programming.dev • 1 year agomessage-square0 Commentsfedilink
synthetic_apriori@programming.devM • edit-21 year agoThe Dafny Programming and Verification Languageplus-squareexternal-linkmessage-square0 fedilinkarrow-up11
arrow-up11external-linkThe Dafny Programming and Verification Languageplus-squaresynthetic_apriori@programming.devM • edit-21 year agomessage-square0 Commentsfedilink
synthetic_apriori@programming.devM • edit-21 year agoBack in June, NASEM hosted a workshop on using AI for mathematical reasoning; many talks discussed the use of AI in developing formal mathematical proofs and formally verifying softwareplus-squareexternal-linkmessage-square0 fedilinkarrow-up11
arrow-up11external-linkBack in June, NASEM hosted a workshop on using AI for mathematical reasoning; many talks discussed the use of AI in developing formal mathematical proofs and formally verifying softwareplus-squaresynthetic_apriori@programming.devM • edit-21 year agomessage-square0 Commentsfedilink
demesisx@programming.dev • edit-21 year agocategory-theory: An axiom-free formalization of category theory in Coq for personal study and practical work by John Wiegleyplus-squareexternal-linkmessage-square0 fedilinkarrow-up11
arrow-up11external-linkcategory-theory: An axiom-free formalization of category theory in Coq for personal study and practical work by John Wiegleyplus-squaredemesisx@programming.dev • edit-21 year agomessage-square0 Commentsfedilink
Ategon@programming.devM • edit-21 year agoWelcome to /c/formal_methods!plus-squaremessage-squaremessage-square0 fedilinkarrow-up11
arrow-up11message-squareWelcome to /c/formal_methods!plus-squareAtegon@programming.devM • edit-21 year agomessage-square0 Commentsfedilink