cyph3rPunk@infosec.pub · edit-22 months agoVerified Effectful Programming in F* - Catalin Hritcuplus-squareyoutu.beexternal-linkmessage-square0fedilinkarrow-up16
arrow-up16external-linkVerified Effectful Programming in F* - Catalin Hritcuplus-squareyoutu.becyph3rPunk@infosec.pub · edit-22 months agomessage-square0fedilink
armchair_progamer@programming.dev · 6 months agoLinearizability! Refinement! Prophecy! (proving code correctness)plus-squaresurfingcomplexity.blogexternal-linkmessage-square0fedilinkarrow-up14
arrow-up14external-linkLinearizability! Refinement! Prophecy! (proving code correctness)plus-squaresurfingcomplexity.blogarmchair_progamer@programming.dev · 6 months agomessage-square0fedilink
armchair_progamer@programming.dev · edit-27 months agoThe Hitchhiker’s Guide to Logical Verification (book)plus-squarebrowncs1951x.github.ioexternal-linkmessage-square0fedilinkarrow-up13
arrow-up13external-linkThe Hitchhiker’s Guide to Logical Verification (book)plus-squarebrowncs1951x.github.ioarmchair_progamer@programming.dev · edit-27 months agomessage-square0fedilink
armchair_progamer@programming.dev · 8 months agoA curated list of awesome Rust checkersplus-squareburtonqin.github.ioexternal-linkmessage-square0fedilinkarrow-up13
arrow-up13external-linkA curated list of awesome Rust checkersplus-squareburtonqin.github.ioarmchair_progamer@programming.dev · 8 months agomessage-square0fedilink
armchair_progamer@programming.dev · edit-28 months agoModeling B-trees in TLA+plus-squaresurfingcomplexity.blogexternal-linkmessage-square0fedilinkarrow-up13
arrow-up13external-linkModeling B-trees in TLA+plus-squaresurfingcomplexity.blogarmchair_progamer@programming.dev · edit-28 months agomessage-square0fedilink
armchair_progamer@programming.dev · 9 months agoNondeterminism in Formal Specificationplus-squarebuttondown.emailexternal-linkmessage-square0fedilinkarrow-up13
arrow-up13external-linkNondeterminism in Formal Specificationplus-squarebuttondown.emailarmchair_progamer@programming.dev · 9 months agomessage-square0fedilink
armchair_progamer@programming.dev · 9 months agoDiffusion On Syntax Trees For Program Synthesis tree-diffusion.github.ioexternal-linkmessage-square0fedilinkarrow-up13
arrow-up13external-linkDiffusion On Syntax Trees For Program Synthesis tree-diffusion.github.ioarmchair_progamer@programming.dev · 9 months agomessage-square0fedilink
armchair_progamer@programming.dev · 10 months agoSome notes on Rust, mutable aliasing and formal verificationplus-squaregraydon2.dreamwidth.orgexternal-linkmessage-square0fedilinkarrow-up13
arrow-up13external-linkSome notes on Rust, mutable aliasing and formal verificationplus-squaregraydon2.dreamwidth.orgarmchair_progamer@programming.dev · 10 months agomessage-square0fedilink
armchair_progamer@programming.dev · 10 months agocoq-of-rust: convert Rust programs into Coq definitions to formally reason about themplus-squaregithub.comexternal-linkmessage-square0fedilinkarrow-up12
arrow-up12external-linkcoq-of-rust: convert Rust programs into Coq definitions to formally reason about themplus-squaregithub.comarmchair_progamer@programming.dev · 10 months agomessage-square0fedilink
armchair_progamer@programming.dev · 10 months agoAgda Core: The Dream and the Realityplus-squarejesper.cxexternal-linkmessage-square0fedilinkarrow-up14
arrow-up14external-linkAgda Core: The Dream and the Realityplus-squarejesper.cxarmchair_progamer@programming.dev · 10 months agomessage-square0fedilink
armchair_progamer@programming.dev · 10 months agoDafny Power User: Type-parameter modes: variance and cardinality preservationplus-squareleino.scienceexternal-linkmessage-square0fedilinkarrow-up13
arrow-up13external-linkDafny Power User: Type-parameter modes: variance and cardinality preservationplus-squareleino.sciencearmchair_progamer@programming.dev · 10 months agomessage-square0fedilink
armchair_progamer@programming.dev · 10 months agoVerus: Verified Rust for low-level systems codeplus-squaregithub.comexternal-linkmessage-square0fedilinkarrow-up14
arrow-up14external-linkVerus: Verified Rust for low-level systems codeplus-squaregithub.comarmchair_progamer@programming.dev · 10 months agomessage-square0fedilink
armchair_progamer@programming.dev · 11 months agoNarya: A proof assistant for higher-dimensional type theory (GitHub)plus-squaregithub.comexternal-linkmessage-square0fedilinkarrow-up13
arrow-up13external-linkNarya: A proof assistant for higher-dimensional type theory (GitHub)plus-squaregithub.comarmchair_progamer@programming.dev · 11 months agomessage-square0fedilink
armchair_progamer@programming.dev · 11 months agoDon't let Alloy facts make your specs a fictionplus-squarewww.hillelwayne.comexternal-linkmessage-square0fedilinkarrow-up13
arrow-up13external-linkDon't let Alloy facts make your specs a fictionplus-squarewww.hillelwayne.comarmchair_progamer@programming.dev · 11 months agomessage-square0fedilink
demesisx@infosec.pubEnglish · 1 year agoVerifiable Random Functionsplus-squareyoutu.beexternal-linkmessage-square0fedilinkarrow-up12
arrow-up12external-linkVerifiable Random Functionsplus-squareyoutu.bedemesisx@infosec.pubEnglish · 1 year agomessage-square0fedilink
armchair_progamer@programming.dev · 1 year agoI formally modeled Dreidel for no good reasonplus-squarebuttondown.emailexternal-linkmessage-square1fedilinkarrow-up13
arrow-up13external-linkI formally modeled Dreidel for no good reasonplus-squarebuttondown.emailarmchair_progamer@programming.dev · 1 year agomessage-square1fedilink
armchair_progamer@programming.dev · 1 year agoTLA+ in Isabelle/HOLplus-squaredavecturner.github.ioexternal-linkmessage-square0fedilinkarrow-up13
arrow-up13external-linkTLA+ in Isabelle/HOLplus-squaredavecturner.github.ioarmchair_progamer@programming.dev · 1 year agomessage-square0fedilink
armchair_progamer@programming.dev · 1 year agorzk: an experimental proof assistant for synthetic ∞-categoriesplus-squarerzk-lang.github.ioexternal-linkmessage-square0fedilinkarrow-up12
arrow-up12external-linkrzk: an experimental proof assistant for synthetic ∞-categoriesplus-squarerzk-lang.github.ioarmchair_progamer@programming.dev · 1 year agomessage-square0fedilink
armchair_progamer@programming.dev · 1 year agoLean/Coq/Isabel and Their Proof Treesplus-squarelakesare.brick.doexternal-linkmessage-square0fedilinkarrow-up13
arrow-up13external-linkLean/Coq/Isabel and Their Proof Treesplus-squarelakesare.brick.doarmchair_progamer@programming.dev · 1 year agomessage-square0fedilink
synthetic_apriori@programming.devM · 2 years agoSo you want to be a proof engineer?plus-squareproofcraft.orgexternal-linkmessage-square0fedilinkarrow-up13
arrow-up13external-linkSo you want to be a proof engineer?plus-squareproofcraft.orgsynthetic_apriori@programming.devM · 2 years agomessage-square0fedilink
