Formal Methods

formal_methods@programming.dev

PostsComments

armchair_progamer@programming.dev · 1 month ago

Linearizability! Refinement! Prophecy! (proving code correctness)

surfingcomplexity.blog

0

3

Linearizability! Refinement! Prophecy! (proving code correctness)

surfingcomplexity.blog

armchair_progamer@programming.dev · 1 month ago

0

armchair_progamer@programming.dev · 3 months ago

The Hitchhiker’s Guide to Logical Verification (book)

browncs1951x.github.io

1

5

The Hitchhiker’s Guide to Logical Verification (book)

browncs1951x.github.io

armchair_progamer@programming.dev · 3 months ago

1

armchair_progamer@programming.dev · 4 months ago

A curated list of awesome Rust checkers

burtonqin.github.io

2

14

A curated list of awesome Rust checkers

burtonqin.github.io

armchair_progamer@programming.dev · 4 months ago

2

armchair_progamer@programming.dev · 4 months ago

Modeling B-trees in TLA+

surfingcomplexity.blog

0

7

Modeling B-trees in TLA+

surfingcomplexity.blog

armchair_progamer@programming.dev · 4 months ago

0

armchair_progamer@programming.dev · 5 months ago

Nondeterminism in Formal Specification

buttondown.email

0

9

Nondeterminism in Formal Specification

buttondown.email

armchair_progamer@programming.dev · 5 months ago

0

armchair_progamer@programming.dev · 5 months ago

Diffusion On Syntax Trees For Program Synthesis

tree-diffusion.github.io

0

5

Diffusion On Syntax Trees For Program Synthesis

tree-diffusion.github.io

armchair_progamer@programming.dev · 5 months ago

0

armchair_progamer@programming.dev · 6 months ago

Some notes on Rust, mutable aliasing and formal verification

graydon2.dreamwidth.org

1

6

Some notes on Rust, mutable aliasing and formal verification

graydon2.dreamwidth.org

armchair_progamer@programming.dev · 6 months ago

1

armchair_progamer@programming.dev · 6 months ago

coq-of-rust: convert Rust programs into Coq definitions to formally reason about them

0

5

coq-of-rust: convert Rust programs into Coq definitions to formally reason about them

armchair_progamer@programming.dev · 6 months ago

0

armchair_progamer@programming.dev · 6 months ago

Agda Core: The Dream and the Reality

0

8

Agda Core: The Dream and the Reality

armchair_progamer@programming.dev · 6 months ago

0

armchair_progamer@programming.dev · 6 months ago

Dafny Power User: Type-parameter modes: variance and cardinality preservation

0

2

Dafny Power User: Type-parameter modes: variance and cardinality preservation

armchair_progamer@programming.dev · 6 months ago

0

armchair_progamer@programming.dev · 6 months ago

Verus: Verified Rust for low-level systems code

1

16

Verus: Verified Rust for low-level systems code

armchair_progamer@programming.dev · 6 months ago

1

armchair_progamer@programming.dev · 7 months ago

Narya: A proof assistant for higher-dimensional type theory (GitHub)

0

7

Narya: A proof assistant for higher-dimensional type theory (GitHub)

armchair_progamer@programming.dev · 7 months ago

0

armchair_progamer@programming.dev · 7 months ago

Don't let Alloy facts make your specs a fiction

www.hillelwayne.com

0

8

Don't let Alloy facts make your specs a fiction

www.hillelwayne.com

armchair_progamer@programming.dev · 7 months ago

0

demesisx@infosec.pubEnglish · 8 months ago

Verifiable Random Functions

0

11

Verifiable Random Functions

demesisx@infosec.pubEnglish · 8 months ago

0

armchair_progamer@programming.dev · 10 months ago

I formally modeled Dreidel for no good reason

buttondown.email

1

17

I formally modeled Dreidel for no good reason

buttondown.email

armchair_progamer@programming.dev · 10 months ago

1

armchair_progamer@programming.dev · 11 months ago

TLA+ in Isabelle/HOL

davecturner.github.io

0

7

TLA+ in Isabelle/HOL

davecturner.github.io

armchair_progamer@programming.dev · 11 months ago

0

armchair_progamer@programming.dev · 1 year ago

rzk: an experimental proof assistant for synthetic ∞-categories

rzk-lang.github.io

0

1

rzk: an experimental proof assistant for synthetic ∞-categories

rzk-lang.github.io

armchair_progamer@programming.dev · 1 year ago

0

armchair_progamer@programming.dev · 1 year ago

Lean/Coq/Isabel and Their Proof Trees

lakesare.brick.do

0

1

Lean/Coq/Isabel and Their Proof Trees

lakesare.brick.do

armchair_progamer@programming.dev · 1 year ago

0

synthetic_apriori@programming.devM · 1 year ago

So you want to be a proof engineer?

0

1

So you want to be a proof engineer?

synthetic_apriori@programming.devM · 1 year ago

0

demesisx@programming.devEnglish · 1 year ago

#239 Grigore Rosu: The K framework - a framework to formally define all programming languages

0

1

#239 Grigore Rosu: The K framework - a framework to formally define all programming languages

demesisx@programming.devEnglish · 1 year ago

0

programming.dev

A collection of programming communities

Welcome Programmers!

programming.dev is a collection of programming communities and other topics relevant to software engineers, hackers, roboticists, hardware and software enthusiasts, and more.

The site is primarily english with some communities in other languages. We are connected to many other sites using the activitypub protocol that you can view posts from in the “all” tab while the “local” tab shows posts on our site.

🔗 Site with links to all relevant programming.dev sites

🟩 Not a fan of the default UI? We have alternate frontends we host that you can view the same content from

ℹ️ We have a wiki site that communities can host documents on

⚖️ All users are expected to follow our Code of Conduct and the other various documents on our legal site

❤️ The site is run by a team of volunteers. If youre interested in donating to help fund things such as server costs you can do so here

💬 We have a microblog site aimed towards programmers available at https://bytes.programming.dev

🛠️ We have a forgejo instance for hosting git repositories relating to our site and the fediverse. If you have a project that relates and follows our Code of Conduct feel free to host it there and if you have ideas for things to improve our sites feel free to create issues in the relevant repositories. To go along with the instance we also have a site for sharing small code snippets that might be too small for their own repository.

🌲 We have a discord server and a matrix space for chatting with other members of the community. These are bridged to each other (so you can interact with people using matrix from discord and vice versa.

Fediseer