Transpilers to proofstacks

Stream: CSLib

[Quinn]

There was discussion of interop between Boole and proof stacks like Dafny, Verus, etc. We've been thinking about a "specification nexus" here at BAIF, a unified IR so you don't have to think about natlang->dafny and natlang->verus in a wishy washy language model context, but you isolate the language model to natlang->spec nexus and then have principled, well-understood transpilers from spec nexus to dafny and spec nexus to verus. (and repeat for kani, refinedc, etc).

When can I see actual boole implementation to start playing with this?

[Clark Barrett]

Our target for having an intial version of Boole is early August. We are dependent on Amazon's release of the language framework, which they are working on hard.

[Bas Spitters]

@Quinn if you want to target Rust, then there's a general discussion in the rust ecosystem about a unified spec language. There seems to be consensus that this should be something like rust with a functional semantics, as is used in Hax, Aeneas, Verus, ...
There's a wider discussion on unified Rust Contracts, that have now made it into the rust compiler nightly.

[Alexandre Rademaker]

Hi @Bas Spitters do you have links or references to these discussions? It remains challenging for me to envision a unified spec language that covers different domains.

[Bas Spitters]

https://rust-lang.zulipchat.com/#narrow/channel/183875-wg-formal-methods/topic/Contracts.20and.20functional.20rust/with/510150678
https://rust-lang.zulipchat.com/#narrow/channel/183875-wg-formal-methods/topic/Contracts/with/520726729