Med-Mastodon

2 posts2 participants0 posts today

José A. AlonsoReadings shared July 5, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/07/06-readings_shared_07-05-25" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/07/06-readings_shared_07-05-25</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AI</a> <a href="https://mathstodon.xyz/tags/CoqProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#CoqProver</a> <a href="https://mathstodon.xyz/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalMethods</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/Maxima" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Maxima</a> <a href="https://mathstodon.xyz/tags/PVS" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#PVS</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Rocq</a>

José A. AlonsoFormal methods at NASA: Past, present, and future. ~ Paul Miner, Natasha Neogi. <a href="https://ntrs.nasa.gov/api/citations/20250006044/downloads/NFM_Keynote_STRIVES-psm.pdf" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://ntrs.nasa.gov/api/citations/20250006044/downloads/NFM_Keynote_STRIVES-psm.pdf</a> <a href="https://mathstodon.xyz/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalMethods</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/PVS" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#PVS</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>

rk: it’s hyphen-minus actuallyAnybody have a copy of the SPARK Ada 83 spec? I have the Ada 83 spec, but not SPARK. <a href="https://mastodon.well.com/tags/ada" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ada</a> <a href="https://mastodon.well.com/tags/formalMethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalMethods</a> <a href="https://mastodon.well.com/tags/programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#programming</a>

Python Weekly 🐍A Python frozenset interpretation of Dependent Type Theory<a href="https://www.philipzucker.com/frozenset_dtt/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.philipzucker.com/frozenset_dtt/</a>Discussions: <a href="https://discu.eu/q/https://www.philipzucker.com/frozenset_dtt/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://discu.eu/q/https://www.philipzucker.com/frozenset_dtt/</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/plt" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#plt</a> <a href="https://mastodon.social/tags/programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#programming</a> <a href="https://mastodon.social/tags/python" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#python</a>

Andrew HelwerUnderstandable & predictable performance has its benefits!<a href="https://discuss.systems/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalMethods</a> <a href="https://discuss.systems/tags/TLAPlus" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#TLAPlus</a> <a href="https://discuss.systems/tags/ModelChecking" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ModelChecking</a>

Compsci WeeklyAre We Serious About Using TLA+ For Statistical Properties?<a href="https://emptysqua.re/blog/are-we-serious-about-statistical-properties-tlaplus/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://emptysqua.re/blog/are-we-serious-about-statistical-properties-tlaplus/</a>Discussions: <a href="https://discu.eu/q/https://emptysqua.re/blog/are-we-serious-about-statistical-properties-tlaplus/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://discu.eu/q/https://emptysqua.re/blog/are-we-serious-about-statistical-properties-tlaplus/</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>

Volker StolzChanneling some PhD vacancies from our 🇳🇱 friends:Six fully-funded PhD positions (4 years) in the project "Cyclic Structures in Programs and Proofs – New Harmonies in Software Correctness by Construction"Deadline: Friday, May 23, 2025<a href="https://cyclic-structures.gitlab.io/vacancies/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://cyclic-structures.gitlab.io/vacancies/</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/TheoremProving" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#TheoremProving</a> <a href="https://mastodon.social/tags/NWOnl" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#NWOnl</a>

harryprayivIf you’re a <a href="https://mastodon.social/tags/haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#haskell</a> user or a proponent of <a href="https://mastodon.social/tags/functionalprogramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#functionalprogramming</a> please consider donating to the <a href="https://mastodon.social/tags/Purescript" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Purescript</a> project to keep it alive.It’s a fairly obscure project but, IMO, it is THE language for web <a href="https://mastodon.social/tags/frontend" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#frontend</a>.On top of that, the backend was recently rewritten in <a href="https://mastodon.social/tags/ChezScheme" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ChezScheme</a> which tends to be very popular choice in the <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalmethods</a> world due to its rigor.I see <a href="https://mastodon.social/tags/ghcjs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ghcjs</a> nipping at its heels but IMO, PS will always be a more bespoke and opinionated tool.<a href="https://opencollective.com/purescript/donate" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://opencollective.com/purescript/donate</a>

Formal Methods EuropeAre you develping or using <a href="https://mastodon.acm.org/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalMethods</a>?Then <a href="https://mastodon.acm.org/tags/FM2026" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FM2026</a> is probably interested in your work!Dates (AoE) * Abstracts: 25th Nov 2025 * Papers 2nd Dec 2025 * Conference 20th–22nd May 2026 and Gold Open Access proceedingsDetails:<a href="https://conf.researchr.org/track/fm-2026/fm-2026-research-paper" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://conf.researchr.org/track/fm-2026/fm-2026-research-paper</a>

Formal Methods EuropeAre you develping or using <a href="https://mastodon.acm.org/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalMethods</a>?Then <a href="https://mastodon.acm.org/tags/FM2026" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FM2026</a> is probably interested in your work!Dates (AoE) * Abstracts: 25th Nov 2025 * Papers 2nd Dec 2025 * Conference 20th–22nd May 2026 Gold Open Access proceedingsDetails:<a href="https://conf.researchr.org/track/fm-2026/fm-2026-research-paper" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://conf.researchr.org/track/fm-2026/fm-2026-research-paper</a>

Jan de Muijnck-Hughes*Last Call* I have a <a href="https://discuss.systems/tags/PhD" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#PhD</a> position for UK students, available with myself and <a href="https://types.pl/@bentnib" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@bentnib</a> This project will be looking at developing new methods for asserting the resilience of existing communicating systems by developing new static analysis methods derived from advanced programming language research.*Hard Deadline*: Wednesday 16th April 2025You will belong to <a href="https://mastodon.acm.org/@StrathCyber" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@StrathCyber</a> and <a href="https://mastodon.acm.org/@mspstrath" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@mspstrath</a>, as well as gaining access to <a href="https://mastodon.scot/@spli" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@spli</a> <a href="https://www.strath.ac.uk/studywithus/postgraduateresearchphdopportunities/science/computerinformationsciences/towardstype-drivenassuranceofcommunicatingsystems/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.strath.ac.uk/studywithus/postgraduateresearchphdopportunities/science/computerinformationsciences/towardstype-drivenassuranceofcommunicatingsystems/</a>(Ignore the deadline on the advert)Please spread the words. <a href="https://discuss.systems/tags/dependentTypes" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#dependentTypes</a> <a href="https://discuss.systems/tags/formalMethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalMethods</a> <a href="https://discuss.systems/tags/idris" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#idris</a> <a href="https://discuss.systems/tags/programmingLanguageTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#programmingLanguageTheory</a> <a href="https://discuss.systems/tags/typeTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#typeTheory</a> <a href="https://discuss.systems/tags/idris2" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#idris2</a> <a href="https://discuss.systems/tags/computerSecurity" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#computerSecurity</a> <a href="https://discuss.systems/tags/cybersecurity" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#cybersecurity</a> <a href="https://discuss.systems/tags/securityByDesign" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#securityByDesign</a> <a href="https://discuss.systems/tags/secureByDesign" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#secureByDesign</a>

Python Weekly 🐍"Verified" "Compilation" of "Python" with Knuckledragger, GCC, and Ghidra<a href="https://www.philipzucker.com/knuckle_C_pcode/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.philipzucker.com/knuckle_C_pcode/</a>Discussions: <a href="https://discu.eu/q/https://www.philipzucker.com/knuckle_C_pcode/" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://discu.eu/q/https://www.philipzucker.com/knuckle_C_pcode/</a><a href="https://mastodon.social/tags/assembly" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#assembly</a> <a href="https://mastodon.social/tags/compilers" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#compilers</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/programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#programming</a> <a href="https://mastodon.social/tags/python" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#python</a> <a href="https://mastodon.social/tags/reversing" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#reversing</a>

Formal Methods EuropeThe 27th Symposium on Formal Methods wants your paper!If your work develops or applies <a href="https://mastodon.acm.org/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalMethods</a> then <a href="https://mastodon.acm.org/tags/FM2026" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FM2026</a> is probably interested!Dates (AoE) * Abstracts: 25th Nov 2025 * Papers 2nd Dec 2025 * Conference 20th–22nd May 2026Proceedings in Springer's LNCS FM subline (gold open access) Details:<a href="https://conf.researchr.org/track/fm-2026/fm-2026-research-paper" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://conf.researchr.org/track/fm-2026/fm-2026-research-paper</a>

Hacker NewsSystems Correctness Practices at AWS: Leveraging Formal and Semi-Formal Methods<a href="https://queue.acm.org/detail.cfm?id=3712057" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://queue.acm.org/detail.cfm?id=3712057</a><a href="https://mastodon.social/tags/HackerNews" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#HackerNews</a> <a href="https://mastodon.social/tags/SystemsCorrectness" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#SystemsCorrectness</a> <a href="https://mastodon.social/tags/AWS" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AWS</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/SoftwareEngineering" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#SoftwareEngineering</a> <a href="https://mastodon.social/tags/TechTrends" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#TechTrends</a> <a href="https://mastodon.social/tags/CloudComputing" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#CloudComputing</a>

LobstersClosing Keynote with Leslie Lamport at SCALE 22x: Coding isn't programming <a href="https://lobste.rs/s/zz69lm" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/zz69lm</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://www.socallinuxexpo.org/scale/22x/presentations/closing-keynote-leslie-lamport" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.socallinuxexpo.org/scale/22x/presentations/closing-keynote-leslie-lamport</a>

LobstersIntroducing GREASE: An Open-Source Tool for Uncovering Hidden Vulnerabilities in Binary Code <a href="https://lobste.rs/s/qykkq8" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://lobste.rs/s/qykkq8</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/release" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#release</a> <a href="https://mastodon.social/tags/reversing" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#reversing</a> <a href="https://mastodon.social/tags/security" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#security</a> <a href="https://www.galois.com/articles/introducing-grease" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.galois.com/articles/introducing-grease</a>

vintage screwlisp account<a href="https://mastodon.sdf.org/tags/formalMethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#formalMethods</a> <a href="https://mastodon.sdf.org/tags/gamedev" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#gamedev</a> <a href="https://mastodon.sdf.org/tags/programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#programming</a> <a href="https://mastodon.sdf.org/tags/commonLisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#commonLisp</a> <a href="https://mastodon.sdf.org/tags/acl2" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#acl2</a> <a href="https://mastodon.sdf.org/tags/itch" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#itch</a> <a href="https://lispy-gopher-show.itch.io/lispmoo2/devlog/907091/formal-game-logic" rel="nofollow noopener noreferrer" target="_blank">https://lispy-gopher-show.itch.io/lispmoo2/devlog/907091/formal-game-logic</a>Since yesterday I advocated strong use of defgeneric, defmethod and McCLIM's define-command, here I present just giving lisp's defun to acl2's first order <a href="https://mastodon.sdf.org/tags/logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#logic</a>.I present a batch processing style for using acl2 both in <a href="https://mastodon.sdf.org/tags/shell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#shell</a> and in <a href="https://mastodon.sdf.org/tags/lisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#lisp</a> with a worked example.Thoughts and opinions, gamedevs and logical types?

Compsci Weeklycoq-of-rust: Formal verification tool for Rust<a href="https://github.com/formal-land/coq-of-rust" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://github.com/formal-land/coq-of-rust</a>Discussions: <a href="https://discu.eu/q/https://github.com/formal-land/coq-of-rust" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://discu.eu/q/https://github.com/formal-land/coq-of-rust</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/programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#programming</a> <a href="https://mastodon.social/tags/rustlang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#rustlang</a>

Andrew HelwerReading the new experience report paper "System Correctness Practices at AWS" by <a href="https://fediscience.org/@marcbrooker" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@marcbrooker</a> & Ankush Desai, a successor to 2015 paper "How Amazon Web Services Uses Formal Methods". Documents a whole buffet of industrial formal methods use: P (including new tool PObserve for runtime trace validation), deterministic simulation testing in Rust with the open-sourced Shuttle and Turmoil tools, Dafny, HOL Light, and the open-sourced Kani model-checker for Rust.While TLA⁺ was the most prominent featured tool in the 2015 paper, it's been lost in the crowd here as part of a clear shift toward verifying & testing the actual running code. I think TLA⁺ must carve out a niche for itself in a world where deterministic simulation testing becomes a commodity technology, or it risks losing relevance same as other design-level tools like UML. There are existing case studies on using TLA⁺ for trace validation and model-driven testing, but a lot of effort needs to go into tooling for making such integrations as smooth as possible instead of bespoke one-off projects.<a href="https://dl.acm.org/doi/10.1145/3712057" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://dl.acm.org/doi/10.1145/3712057</a><a href="https://discuss.systems/tags/TLAplus" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#TLAplus</a> <a href="https://discuss.systems/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FormalMethods</a>

Recent searches

Search options

Administered by:

Server stats:

#formalmethods