I always thought that formal verification (FV) of programs would be too hard and error prone beyond simple programs. Apparently I was wrong about that, and one reason is that FV should be applied above the program level - e.g., to algorithms.
*"TLA+ is a language for modeling software above the code level and hardware above the circuit level. It has an IDE (Integrated Development Environment) for writing models and running tools to check them." * Formal Verification With TLA+ <https://lamport.azurewebsites.net/tla/high-level-view.html> -- You received this message because you are subscribed to the Google Groups "leo-editor" group. To unsubscribe from this group and stop receiving emails from it, send an email to leo-editor+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/leo-editor/9430e879-d3a3-4420-944d-e0c491faa147n%40googlegroups.com.
