alt Hacker NewsVerus seems to be exactly what I have been looking for! I discovered AllConcur[0] on HN a while back, and I wanted to port it to Go, but since it used TLA+ and C, and it was very confusing for me to understand how you can trust the implementation unless you can compile TLA+ to C.
I was talking to Gemini about comparing Verus to TLA+ and it said that TLA+ is usually used (for example) "to prove that a distributed consensus protocol is logically sound" but when I asked if Verus can do that too, it said yes. So Verus can be compiled and integrated with Rust, whereas TLA+ is used more for blueprint development that then guides the implementation in the mind of the implementer.
Seems awesome!
Replies
japgolly • today at 4:16 AM
[dead]
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.