armchair_progamer@programming.dev · 14 days agoNondeterminism in Formal Specificationplus-squarebuttondown.emailexternal-linkmessage-square0fedilinkarrow-up19arrow-down10
arrow-up19arrow-down1external-linkNondeterminism in Formal Specificationplus-squarebuttondown.emailarmchair_progamer@programming.dev · 14 days agomessage-square0fedilink
armchair_progamer@programming.dev · 27 days agoDiffusion On Syntax Trees For Program Synthesis tree-diffusion.github.ioexternal-linkmessage-square0fedilinkarrow-up15arrow-down10
arrow-up15arrow-down1external-linkDiffusion On Syntax Trees For Program Synthesis tree-diffusion.github.ioarmchair_progamer@programming.dev · 27 days agomessage-square0fedilink
armchair_progamer@programming.dev · 1 month agoSome notes on Rust, mutable aliasing and formal verificationplus-squaregraydon2.dreamwidth.orgexternal-linkmessage-square1fedilinkarrow-up16arrow-down10
arrow-up16arrow-down1external-linkSome notes on Rust, mutable aliasing and formal verificationplus-squaregraydon2.dreamwidth.orgarmchair_progamer@programming.dev · 1 month agomessage-square1fedilink
armchair_progamer@programming.dev · 2 months agocoq-of-rust: convert Rust programs into Coq definitions to formally reason about themplus-squaregithub.comexternal-linkmessage-square0fedilinkarrow-up15arrow-down10
arrow-up15arrow-down1external-linkcoq-of-rust: convert Rust programs into Coq definitions to formally reason about themplus-squaregithub.comarmchair_progamer@programming.dev · 2 months agomessage-square0fedilink
armchair_progamer@programming.dev · 2 months agoAgda Core: The Dream and the Realityplus-squarejesper.cxexternal-linkmessage-square0fedilinkarrow-up18arrow-down10
arrow-up18arrow-down1external-linkAgda Core: The Dream and the Realityplus-squarejesper.cxarmchair_progamer@programming.dev · 2 months agomessage-square0fedilink
armchair_progamer@programming.dev · 2 months agoDafny Power User: Type-parameter modes: variance and cardinality preservationplus-squareleino.scienceexternal-linkmessage-square0fedilinkarrow-up13arrow-down11
arrow-up12arrow-down1external-linkDafny Power User: Type-parameter modes: variance and cardinality preservationplus-squareleino.sciencearmchair_progamer@programming.dev · 2 months agomessage-square0fedilink
armchair_progamer@programming.dev · 2 months agoVerus: Verified Rust for low-level systems codeplus-squaregithub.comexternal-linkmessage-square1fedilinkarrow-up116arrow-down10
arrow-up116arrow-down1external-linkVerus: Verified Rust for low-level systems codeplus-squaregithub.comarmchair_progamer@programming.dev · 2 months agomessage-square1fedilink
armchair_progamer@programming.dev · 2 months agoNarya: A proof assistant for higher-dimensional type theory (GitHub)plus-squaregithub.comexternal-linkmessage-square0fedilinkarrow-up17arrow-down10
arrow-up17arrow-down1external-linkNarya: A proof assistant for higher-dimensional type theory (GitHub)plus-squaregithub.comarmchair_progamer@programming.dev · 2 months agomessage-square0fedilink
armchair_progamer@programming.dev · 3 months agoDon't let Alloy facts make your specs a fictionplus-squarewww.hillelwayne.comexternal-linkmessage-square0fedilinkarrow-up18arrow-down10
arrow-up18arrow-down1external-linkDon't let Alloy facts make your specs a fictionplus-squarewww.hillelwayne.comarmchair_progamer@programming.dev · 3 months agomessage-square0fedilink
demesisx@infosec.pubEnglish · 4 months agoVerifiable Random Functionsplus-squareyoutu.beexternal-linkmessage-square0fedilinkarrow-up111arrow-down10
arrow-up111arrow-down1external-linkVerifiable Random Functionsplus-squareyoutu.bedemesisx@infosec.pubEnglish · 4 months agomessage-square0fedilink
armchair_progamer@programming.dev · 6 months agoI formally modeled Dreidel for no good reasonplus-squarebuttondown.emailexternal-linkmessage-square1fedilinkarrow-up119arrow-down12
arrow-up117arrow-down1external-linkI formally modeled Dreidel for no good reasonplus-squarebuttondown.emailarmchair_progamer@programming.dev · 6 months agomessage-square1fedilink
armchair_progamer@programming.dev · 6 months agoTLA+ in Isabelle/HOLplus-squaredavecturner.github.ioexternal-linkmessage-square0fedilinkarrow-up17arrow-down10
arrow-up17arrow-down1external-linkTLA+ in Isabelle/HOLplus-squaredavecturner.github.ioarmchair_progamer@programming.dev · 6 months agomessage-square0fedilink
armchair_progamer@programming.dev · 9 months agorzk: an experimental proof assistant for synthetic ∞-categoriesplus-squarerzk-lang.github.ioexternal-linkmessage-square0fedilinkarrow-up17arrow-down10
arrow-up17arrow-down1external-linkrzk: an experimental proof assistant for synthetic ∞-categoriesplus-squarerzk-lang.github.ioarmchair_progamer@programming.dev · 9 months agomessage-square0fedilink
armchair_progamer@programming.dev · 9 months agoLean/Coq/Isabel and Their Proof Treesplus-squarelakesare.brick.doexternal-linkmessage-square0fedilinkarrow-up14arrow-down10
arrow-up14arrow-down1external-linkLean/Coq/Isabel and Their Proof Treesplus-squarelakesare.brick.doarmchair_progamer@programming.dev · 9 months agomessage-square0fedilink
synthetic_apriori@programming.devM · 11 months agoSo you want to be a proof engineer?plus-squareproofcraft.orgexternal-linkmessage-square0fedilinkarrow-up13arrow-down10
arrow-up13arrow-down1external-linkSo you want to be a proof engineer?plus-squareproofcraft.orgsynthetic_apriori@programming.devM · 11 months agomessage-square0fedilink
demesisx@programming.devEnglish · 11 months ago#239 Grigore Rosu: The K framework - a framework to formally define all programming languagesplus-squareyoutu.beexternal-linkmessage-square0fedilinkarrow-up12arrow-down10
arrow-up12arrow-down1external-link#239 Grigore Rosu: The K framework - a framework to formally define all programming languagesplus-squareyoutu.bedemesisx@programming.devEnglish · 11 months agomessage-square0fedilink
synthetic_apriori@programming.devM · edit-21 year agoThe Dafny Programming and Verification Languageplus-squaredafny.orgexternal-linkmessage-square0fedilinkarrow-up11arrow-down10
arrow-up11arrow-down1external-linkThe Dafny Programming and Verification Languageplus-squaredafny.orgsynthetic_apriori@programming.devM · edit-21 year agomessage-square0fedilink
synthetic_apriori@programming.devMEnglish · 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-squarewww.nationalacademies.orgexternal-linkmessage-square0fedilinkarrow-up11arrow-down10
arrow-up11arrow-down1external-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-squarewww.nationalacademies.orgsynthetic_apriori@programming.devMEnglish · edit-21 year agomessage-square0fedilink
demesisx@programming.devEnglish · edit-21 year agocategory-theory: An axiom-free formalization of category theory in Coq for personal study and practical work by John Wiegleyplus-squaregithub.comexternal-linkmessage-square0fedilinkarrow-up13arrow-down10
arrow-up13arrow-down1external-linkcategory-theory: An axiom-free formalization of category theory in Coq for personal study and practical work by John Wiegleyplus-squaregithub.comdemesisx@programming.devEnglish · edit-21 year agomessage-square0fedilink
Ategon@programming.devMEnglish · edit-21 year agoWelcome to /c/formal_methods!plus-squaremessage-squaremessage-square0fedilinkarrow-up11arrow-down10
arrow-up11arrow-down1message-squareWelcome to /c/formal_methods!plus-squareAtegon@programming.devMEnglish · edit-21 year agomessage-square0fedilink