Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
mastodon.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
The original server operated by the Mastodon gGmbH non-profit

Administered by:

Server stats:

354K
active users

mastodon.social: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.4.0-nightly.2025-03-25

#formalmethods

3 posts2 participants0 posts today
Public *
Cass Alexandru

The other thing that I really enjoyed in my industry job is to really think that, hey, the skills that we have as PL people and as formal methods, functional programming, these sorts of things, they are relevant. It’s like people say that when you get into industry, these things are not important. And I think that’s a total misconception. It’s a total lie because, of course, if you don’t know what you can do with a nice systematic approach, of course, you don’t end up doing it, and everything becomes just another hack. - Farhad Mehta – the Haskell Interlude Podcast
#haskell #FunctionalProgramming #formalmethods

haskell.foundationFarhad MehtaIn this episode, Andres Löh and Mike Sperber are joined by Farhad Mehta, a professor at OST Rapperswil, and one of the organizers of ZuriHac. Farhad tells us about formal methods, building tunnels, the importance of education, and the complicated relationship between academia and industry.
Public
screwlisp

#formalMethods #gamedev #programming #commonLisp #acl2 #itch lispy-gopher-show.itch.io/lisp

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 #logic.

I present a batch processing style for using acl2 both in #shell and in #lisp with a worked example.

Thoughts and opinions, gamedevs and logical types?

itch.io(formal) game logic - lispmoo2 by screwtape1. Intro This begins part 2 of https://lispy-gopher-show.itch.io/lispmoo2/devlog/906389/my-programming-principles-for-game-dev-12 . Which contains the first five parts. These second five parts contain...
Public
Andrew Helwer

Reading the new experience report paper "System Correctness Practices at AWS" by @marcbrooker & 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.

dl.acm.org/doi/10.1145/3712057

QueueSystems Correctness Practices at AWS: Leveraging Formal and Semi-formal Methods: Queue: Vol 22, No 6 Building reliable and secure software requires a range of approaches to reason about systems correctness. Alongside industry-standard testing methods (such as unit and integration testing), AWS has adopted model checking, fuzzing, property-based testing, ...
#TLAplus#FormalMethods
ExploreLive feeds
About