Nondeterminism is used very often in formal specifications, and not just when multi-threading or explicit randomness are involved. This article provides examples, insight into why that is, and more.

Recently Boats wrote a blog post about Rust, mutable aliasing, and the sad story of local reasoning over many decades of computer science. I recommend that post and agree with its main points! Go read it! But I also thought I'd add a little more detail to an area it's less acutely focused on: formal methods / formal verification.

TL;DR: support for local reasoning is a big factor in the ability to do automated reasoning about programs. Formal verification involves such reasoning. Rust supports it better than many other imperative systems languages -- even some impure functional ones! -- and formal verification people are excited and building tools presently. This is not purely by accident, and is worth understanding as part of what makes Rust valuable beyond "it doesn't need a GC".

The rest of this post is just unpacking and giving details of one or more of the above assertions, which I'll try to address in order of plausible interestingness to the present, but I will also throw in some history because I kinda can't help myself.

The author is Graydon Hoare, the "founder" of Rust and technical lead until around 2013.

From README:

At the heart of coq-of-rust is the translation of Rust programs to the proof system Coq 🐓. Once some Rust code is translated to Coq, it can then be verified using standard proof techniques.

Here is an example of a Rust function:

fn add_one(x: u32) -> u32 {
    x + 1
}

Running coq-of-rust, it translates in Coq to:

Definition add_one (τ : list Ty.t) (α : list Value.t) : M :=
  match τ, α with
  | [], [ x ] =>
    ltac:(M.monadic
      (let x := M.alloc (| x |) in
      BinOp.Panic.add (| M.read (| x |), Value.Integer Integer.U32 1 |)))
  | _, _ => M.impossible
  end.

Functions such as BinOp.Panic.add are part of the standard library for Rust in Coq that we provide. We can then express and verify specifications on the code in Coq.

Blog:

• Improvements in the Rust translation to Coq, part 1, part 2, part 3
• Monadic notation for the Rust translation
• Translation of Rust's core and alloc crates

The same group also recently started coq-of-python, which is the same thing but for Python:

• Translation of Python code to Coq
• Simulation of Python code in Coq

Alternate Rust-to-_ translators:

• Hax: Translate Rust to Coq (like above) or F*.
• Aeneas + Charon: Translate Rust's MIR to pure lambda calculus / F* / Coq / HOL / Lean. Currently has some strict limitations like no nested loops or closures. Paper: Aeneas: Rust verification by functional translation.

Other Rust formal verification projects:

• Creusot: Formally verifies Rust code with annotations representing preconditions/postconditions/assertions, by translating the MIR to Why3 then solving.
• Kani: Formally verifies Rust code with annotations, by using model checking powered by CBMC.
• Verus: Formally verifies a Rust DSL with syntax extensions to represent preconditions/postconditions/assertions, by using the Z3 SMT solver.

This blog post is about Agda Core, a project to build a a formally specified core language for (a reasonable subset of) Agda together with a reference implementation of a type checker for it. If you have been following my work, you might know that I have been working on this project on and off for the past few years, yet the current version is still very much a work in progress. Hence, in the second part of this post, I will dive into a few examples of some of the more unexpected and interesting obstacles we encountered while trying to turn Agda Core from a dream into reality.

Context: Dafny is a programming language with a built-in SMT solver that can encode formally-checked statements (e.g. preconditions, postconditions, assertions).

Dafny has features of most programming languages; for example, covariant/contravariant/"non-variant" (invariant) type parameters. But in order to keep said verification sound and decidable in reasonable time, these features have extra restrictions and other complexities.

This article explains that there are 2 more "variance modes", because the of "covariant" and "invariant" variances may be "cardinality-preserving" or "not cardinality-preserving".

// Most "traditional" languages have 3 variances
type Foo<
    +CovariantParameter,
    NonVariantParameter,
    -ContravariantParameter>
// Dafny has 5
type Bar<
    +CovariantCardinalityPreservingParameter, 
    NonVariantCardinalityPreservingParameter,
    -ContravariantParameter, 
    *CovariantNonCardinalityPreservingParameter, 
    !NonVariantNonCardinalityPreservingParameter>

Another, very similar verified superset of Rust is Creusot. I'm not sure what the benefits/downsides of each are besides syntax tbh.

This is also similar to Kani which also verifies Rust code. However, Kani is a model checker like TLC (the model checker for TLA+), while Verus and Creusot are SMT solvers like Dafny.

Interestingly, Verus (unlike both Kani and Creusot) has its language server, which is a fork of rust-analyzer (verus-analyzer).

Narya is eventually intended to be a proof assistant implementing Multi-Modal, Multi-Directional, Higher/Parametric/Displayed Observational Type Theory, but a formal type theory combining all those adjectives has not yet been specified. At the moment, Narya implements a normalization-by-evaluation algorithm and typechecker for an observational-style theory with Id/Bridge types satisfying parametricity, of variable arity and internality. There is a parser with user-definable mixfix notations, and user-definable record types, inductive datatypes and type families, and coinductive codatatypes, with functions definable by matching and comatching case trees.

cross-posted from: https://infosec.pub/post/9524990

Verifiable Random Functions

It uses PRISM, a "probabilistic model checker", so not your typical theorem prover or SAT solver.

In the past few years, we witnessed the development of multiple smart contract languages - Solidity, Viper, Michelson, Scilla etc. These languages need to enable developers to write correct, predictable behavior smart contract code. Each language development effort therefore ends up spending resources into building formal verification toolsets, compilers, debuggers and other developer tools. In this episode, we are joined by Grigore Rosu, Professor of computer science at UIUC [University of Illinois at Urbana-Champaign] for a deep dive into the K framework. The K framework is mathematic logic and language that enables language developers to formally define all programming languages; such as C, Solidity and JavaScript. Once a language is formally specified in the K framework, the framework automatically outputs a range of formal verification toolsets, compilers, debuggers and other developer tools for it. Updates to the language can be made directly in K. This technology has massive implications for smart contract programming language development, and formal verification efforts in the blockchain space. We also cover his efforts to express the Ethereum virtual machine using the K framework, and to develop a new virtual machine technology, called IELE, specifically tailored to the blockchain space. Check out the episode to understand a game changing technology in the formal verification and smart contract safety space.

Topics discussed in this episode:

• Grigore's background with NASA and work on formally verified correct software
• Motivations to develop K framework
• Basic principles behind the operation of K framework
• How K deals with undefined behavior / ambiguities in a language definition
• The intersection of K framework and smart contract technology
• Runtime Verification's collaboration with Cardano
• KEVM and IELE, smart contract virtual machines developed by Runtime Verification
• Broader implications of the K framework for the blockchain industry

I saw this posted on r/ProgrammingLanguages. I hadn't heard of this language before, but it looks neat.

https://en.wikipedia.org/wiki/Dafny

Recordings are available here: https://www.nationalacademies.org/event/06-12-2023/ai-to-assist-mathematical-reasoning-a-workshop

This development encodes category theory in Coq, with the primary aim being to allow representation and manipulation of categorical terms, as well realization of those terms in various target categories.

The community currently has no mods (as the person who requested it in the request community did not want to mod it).

If anyone wants to be a mod feel free to dm me or reply here