4 ms·
That is my pet peeve against TLA+ advocacy, the disassociation between a theoretical proof of a specific algorithm, data structures, and the actual implementati
by pjmlp 16d ago
That is my pet peeve against TLA+ advocacy, the disassociation between a theoretical proof of a specific algorithm, data structures, and the actual implementation in production.
I rather push for tooling that allows code generation based on the formal proofs like FStart or Dafny, or is integrated with specific programming languages like SPARK, Frama-C or this Verus.
- igornotarobot 16d agoYou can write everything in Lean and generate an implementation. Given that LLMs can now generate Lean proofs, this does not seem to be prohibitively expensive anymore. The real issue with distributed algorithms is that they are hard to reason about, and reasoning about them at the code level does not make the verification problem easier, it makes it harder.
- kreneskyp 15d agoI'm working on a ISO-29148 aligned spec standard with formal modelling baked in. It's meant to sit above the code with types, contracts, proofs and other objects that lower mechanically into code and/or are deterministically verified. I'm targeting Rust primarily but my goal is that any language could sit under it via an integration layer. https://github.com/agent-ix/quoin https://github.com/agent-ix/quoin The first public version of the formal specification standard isn't available yet. Pushing hard to get it out soon! But Quoin ships with an earlier version of the spec standard. It features derived property tests, which was the POC for fully adopting a formal-spec-to-derived-formal-verification ecosystem.
- pjmlp 15d agoThanks for sharing, always like to learn about this stuff.