Mastouille

5 messages3 participants2 messages aujourd’hui

Lobsters“Bad Apple!!” But It’s 3288 Lean Tactics Spamming VSCode <a href="https://lobste.rs/s/ccvkpv" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/ccvkpv</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://mastodon.social/tags/graphics" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#graphics</a> <a href="https://unnamed.website/posts/bad-apple-lean-tactic/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://unnamed.website/posts/bad-apple-lean-tactic/</a>

LobstersMy first verified (imperative) program via <a href="https://social.treehouse.systems/@RunxiYu" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@RunxiYu</a> <a href="https://lobste.rs/s/giycc1" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/giycc1</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://mastodon.social/tags/plt" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#plt</a> <a href="https://markushimmel.de/blog/my-first-verified-imperative-program/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://markushimmel.de/blog/my-first-verified-imperative-program/</a>

LobstersA supposedly worthwhile contract I'll never do again by <a href="https://discuss.systems/@ahelwer" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@ahelwer</a> <a href="https://lobste.rs/s/zhiv3y" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/zhiv3y</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://ahelwer.ca/post/2025-07-04-tla-contracts/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://ahelwer.ca/post/2025-07-04-tla-contracts/</a>

LobstersRapid Prototyping a Safe, Logless Reconfiguration Protocol for MongoDB with TLA+ <a href="https://lobste.rs/s/teixnn" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/teixnn</a> <a href="https://mastodon.social/tags/distributed" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#distributed</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://www.mongodb.com/blog/post/technical/rapid-prototyping-safe-logless-reconfiguration-protocol-mongodb-tla-plus" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.mongodb.com/blog/post/technical/rapid-prototyping-safe-logless-reconfiguration-protocol-mongodb-tla-plus</a>

LobstersInequality Union Finds: Baby Steps to Refinement E-graphs by <a href="https://types.pl/@sandmouth" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@sandmouth</a> <a href="https://lobste.rs/s/wahapd" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/wahapd</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://mastodon.social/tags/plt" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#plt</a> <a href="https://www.philipzucker.com/le_find/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.philipzucker.com/le_find/</a>

LobstersProving that every program halts <a href="https://lobste.rs/s/l280ru" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/l280ru</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://mastodon.social/tags/satire" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#satire</a> <a href="https://ntietz.com/blog/proving-that-every-program-halts/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://ntietz.com/blog/proving-that-every-program-halts/</a>

LobstersTelescopes Are Tries: A Dependent Type Shellac on SQLite by <a href="https://types.pl/@sandmouth" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@sandmouth</a> <a href="https://lobste.rs/s/u6xhiw" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/u6xhiw</a> <a href="https://mastodon.social/tags/databases" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#databases</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://mastodon.social/tags/plt" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#plt</a> <a href="https://www.philipzucker.com/telescope_tries/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.philipzucker.com/telescope_tries/</a>

LobstersStarMalloc: verified memory allocator <a href="https://lobste.rs/s/jpfyd6" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/jpfyd6</a> <a href="https://mastodon.social/tags/compsci" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#compsci</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://mastodon.social/tags/security" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#security</a> <a href="https://dl.acm.org/doi/10.1145/3689773" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://dl.acm.org/doi/10.1145/3689773</a>

Lobsters100 years of Zermelo’s axiom of choice: What was the problem with it? <a href="https://lobste.rs/s/kbcp5p" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/kbcp5p</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://mastodon.social/tags/math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#math</a> <a href="https://research.mietek.io/mi.MartinLof2006.html" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://research.mietek.io/mi.MartinLof2006.html</a>

LobstersWriting a Verified Postfix Calculator in Ada/SPARK <a href="https://lobste.rs/s/uwhv3o" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/uwhv3o</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://mastodon.social/tags/programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#programming</a> <a href="https://pyjarrett.github.io/2025/06/10/postfix-calculator.html" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://pyjarrett.github.io/2025/06/10/postfix-calculator.html</a>

LobstersProving completeness of an eventually perfect failure detector in Lean4 <a href="https://lobste.rs/s/adl5af" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/adl5af</a> <a href="https://mastodon.social/tags/distributed" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#distributed</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://protocols-made-fun.com/lean/2025/06/10/lean-epfd-completeness.html" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://protocols-made-fun.com/lean/2025/06/10/lean-epfd-completeness.html</a>

LobstersRewriting SymCrypt in Rust to modernize Microsoft’s cryptographic library <a href="https://lobste.rs/s/p8uq6e" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/p8uq6e</a> <a href="https://mastodon.social/tags/c" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#c</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://mastodon.social/tags/rust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#rust</a> <a href="https://www.microsoft.com/en-us/research/blog/rewriting-symcrypt-in-rust-to-modernize-microsofts-cryptographic-library/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.microsoft.com/en-us/research/blog/rewriting-symcrypt-in-rust-to-modernize-microsofts-cryptographic-library/</a>

LobstersPassing of Jean-Raymond Abrial <a href="https://lobste.rs/s/hao2zr" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/hao2zr</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://en.wikipedia.org/wiki/Jean-Raymond_Abrial" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://en.wikipedia.org/wiki/Jean-Raymond_Abrial</a>

LobstersLightweight Diagramming for Lightweight Formal Methods <a href="https://lobste.rs/s/mgdqwx" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/mgdqwx</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://blog.brownplt.org/2025/06/09/copeanddrag.html" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://blog.brownplt.org/2025/06/09/copeanddrag.html</a>

LobstersNVIDIA ISO-26262 SPARK Process <a href="https://lobste.rs/s/mkivgh" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/mkivgh</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://mastodon.social/tags/practices" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#practices</a> <a href="https://mastodon.social/tags/release" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#release</a> <a href="https://nvidia.github.io/spark-process/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://nvidia.github.io/spark-process/</a>

Haskell WeeklyWhat Works (and Doesn't) Selling Formal Methods<a href="https://www.galois.com/articles/what-works-and-doesnt-selling-formal-methods" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.galois.com/articles/what-works-and-doesnt-selling-formal-methods</a>Discussions: <a href="https://discu.eu/q/https://www.galois.com/articles/what-works-and-doesnt-selling-formal-methods" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://discu.eu/q/https://www.galois.com/articles/what-works-and-doesnt-selling-formal-methods</a><a href="https://mastodon.social/tags/compsci" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#compsci</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://mastodon.social/tags/haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#haskell</a> <a href="https://mastodon.social/tags/programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#programming</a>

LobstersAI is a gamechanger for TLA+ users <a href="https://lobste.rs/s/mp34xp" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/mp34xp</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://mastodon.social/tags/vibecoding" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#vibecoding</a> <a href="https://buttondown.com/hillelwayne/archive/ai-is-a-gamechanger-for-tla-users/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://buttondown.com/hillelwayne/archive/ai-is-a-gamechanger-for-tla-users/</a>

LobstersConformance Checking at MongoDB: Testing That Our Code Matches Our TLA+ Specs | MongoDB Blog <a href="https://lobste.rs/s/giqysi" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/giqysi</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://www.mongodb.com/blog/post/engineering/conformance-checking-at-mongodb-testing-our-code-matches-our-tla-specs" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.mongodb.com/blog/post/engineering/conformance-checking-at-mongodb-testing-our-code-matches-our-tla-specs</a>

LobstersA Lean companion to “Analysis I” via <a href="https://mathstodon.xyz/@mseri" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@mseri</a> <a href="https://lobste.rs/s/rzvbe9" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/rzvbe9</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://mastodon.social/tags/math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#math</a> <a href="https://terrytao.wordpress.com/2025/05/31/a-lean-companion-to-analysis-i/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://terrytao.wordpress.com/2025/05/31/a-lean-companion-to-analysis-i/</a>

LobstersSystems Correctness Practices at Amazon Web Services <a href="https://lobste.rs/s/giokgl" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/giokgl</a> <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> <a href="https://mastodon.social/tags/testing" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#testing</a> <a href="https://cacm.acm.org/practice/systems-correctness-practices-at-amazon-web-services/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://cacm.acm.org/practice/systems-correctness-practices-at-amazon-web-services/</a>

Recherches récentes

Options de recherche

Administré par :

Statistiques du serveur :

#formalmethods