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