Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
mastodon.world is one of the many independent Mastodon servers you can use to participate in the fediverse.
Generic Mastodon server for anyone to use.

Administered by:

Server stats:

8.9K
active users

mastodon.world: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.8

#formalverification

1 post1 participant0 posts today
Public
Jan :rust: :ferris:

People of ACM - Derek Dreyer

acm.org/articles/people-of-acm

"Derek Dreyer is a Scientific Director at the Max Planck Institute for Software Systems (MPI-SWS) [...]. His [...] interests include type systems, semantics of programming languages, verification of concurrent programs, and interactive theorem proving. [...] His goal is “to produce rigorous formal foundations for establishing the safety and reliability of software systems.”"

www.acm.orgPeople of ACM - Derek DreyerDerek Dreyer is a Scientific Director at the Max Planck Institute for Software Systems (MPI-SWS) in Saarbrücken, Germany. At MPI-SWS, he leads the Foundations of Programming Group. His broad range of interests include type systems, semantics of programming languages, verification of concurrent programs, and interactive theorem proving. In his research statement, Dreyer writes that his goal is “to produce rigorous formal foundations for establishing the safety and reliability of software systems.”
#FormalVerification#Rust#RustLang
Public
Jan :rust: :ferris:

(❁´◡`❁)

#Rust pattern types RFC:
gist.github.com/joboet/0cecbce

Pattern types are a form of refinement types, which allow some subset of #FormalVerification!

en.wikipedia.org/wiki/Refineme

Tracking Issue for #PatternTypes:
github.com/rust-lang/rust/issu

Tracking Issue for generic pattern types OwO:
github.com/rust-lang/rust/issu

Implement minimal, internal-only pattern types in the type system:
github.com/rust-lang/rust/pull

I'm _really_ looking forward to how #RustLang will evolve in this area!👀

Pattern types RFC. GitHub Gist: instantly share code, notes, and snippets.
GistPattern types RFCPattern types RFC. GitHub Gist: instantly share code, notes, and snippets.
#ProgrammingLanguage
Public
Lean

The Department of Computer Science, University of Oxford has released recordings of the recent Strachey Series Lectures featuring Leo de Moura and Kevin Buzzard:

1️⃣ "Formalizing the Future: Lean's Impact on Mathematics, Programming, and AI" - Leo de Moura, Chief Architect of Lean

Leo discusses how Lean provides a framework for machine-checkable mathematical proofs and code verification, enabling collaboration between mathematicians, software developers, and AI systems. He also outlines the work the Lean Focused Research Organization does to expand Lean’s capabilities and support the community.

➡️ Watch Leo's lecture here: podcasts.ox.ac.uk/formalizing-

2️⃣ "Will Computers Prove Theorems?" with Kevin Buzzard, Professor of Mathematics, Imperial College

Kevin examines the potential for AI systems and theorem provers to assist in mathematical discovery, addressing whether computers might someday find patterns in mathematics that humans have missed, and discusses the integration of language models with formal verification systems.

➡️ Watch Kevin's lecture here: podcasts.ox.ac.uk/will-compute

podcasts.ox.ac.ukFormalizing the Future: Lean’s Impact on Mathematics, Programming, and AIHow can mathematicians, software developers, and AI systems work together with complete confidence in each other’s contributions? The open-source Lean proof assistant and programming language provides an answer, offering a rigorous framework where proofs and programs are machine-checkable, shared, and extended by a broad community of collaborators. By removing the traditional reliance on trust-based verification and manual oversight, Lean not only accelerates research and development but also redefines how we collaborate.
#LeanLang#LeanProver#FormalVerification
Public *
Lean

The Lean FRO team met synchronously in Amsterdam last week for our annual team retreat, and to discuss upcoming work and our Year 3 roadmap! 🇳🇱✨

We had very productive discussions around Lean's future in mathematics, software and hardware verification, and AI for math. It was energizing to see our team's commitment to Lean's continued growth in each of these domains.

We're cooking up many exciting developments that will support both our mathematical community and our growing base of software verification users. Stay tuned for our full Y3 roadmap publication at the end of July!

The Lean logo in uppercase letters with backwards E, representing the mathematical symbol "there exists", and upside down A, representing the mathematical symbol "for all".
#LeanLang#LeanProver#Lean4
Public
Jan :rust: :ferris:

F* (fstar) Interactive Tutorial:

fstar-lang.org/tutorial/

I'm only like 10% into the tutorial, but this language is CRAZY (fun)! :awesome: 😄

I try to learn the fundamentals of it, so I can use the backend of it in #Aeneas... so I can ultimately formally verify my #Rust crate (former attempts with #Creusot and #Kani failed for me).

Aeneas:
github.com/AeneasVerif/aeneas

See part two of toot for a toy example of proving function equivalence

1/2

fstar-lang.orgF* Tutorial
#FormalVerification#FunctionalProgramming#RustLang
Continued thread
Public
Jan :rust: :ferris:

Huh, seems like I really have been living on the bleeding edge (of #FormalVerification):

github.com/creusot-rs/creusot/

The verification in the prev toot is currently not possible in #Creusot due to missing specs for the `Hash` trait and HashMap more broadly. 😔

Oh well, seems like (at least currently!) I won't be able to fully verify the diffing algorithm of #CSVDiff.🥺

Options I have now are:
- Only verify parts of the algorithm (that don't depend on HashMap ops)
or
- Use fuzzing/property testing

Public
Jan :rust: :ferris:

Place Capability Graphs: A General-Purpose Model of #Rust’s
Ownership and Borrowing Guarantees (April 2025)

arxiv.org/pdf/2503.21691

"We present a novel model of Rust’s type-checking [...], which lifts [...] limitations [of current verification tools], and which can be directly calculated from the #RustLang compiler’s own programmatic representations and analyses. We demonstrate that our model supports over 98% of Rust functions in the most popular public crates...

1/2

#FormalVerification
Continued thread
Public
Jan :rust: :ferris:

Re: Help us create a vision for Rust's future 👆

In the mid- to long-term I can see #Rust focus more and more on facilitating #FormalVerification - it perfectly aligns with #RustLang's vision of enabling everyone to build _reliable_ and efficient software.

First step is probably to have a common contract language, which might enable interoperability of different verification tools.

(Disclaimer: I'm a total newbie in the field of formal verification, but I find it absolutely fascinating!)

ExploreLive feeds
About