|
|
|
|
|
|
by smallnamespace
3629 days ago
|
|
|
> I could just write the code for that but I'll never prove the system works that way. Or you could just prove from first principles, like we all learn in formal algorithm design theory. The question is not whether proofs are valuable, the question is whether translating a system into TLA and using that proof checker is more reliable and saves you time over just attempting a proof directly. Even if your TLA proof checks out, it may be a false positive because it doesn't accurately reflect your production code. |
|
|
What TLA+ and other languages give you is an automated theorem prover or model checked that usually is built on some form of temporal logic and predicate calculus. This is especially good at modelling multiple communicating processes. Taking a logical approach to discrete maths has a few benefits here.
> Even if your TLA proof checks out, it may be a false positive because it doesn't accurately reflect your production code.
This is something one needs to be concerned with when writing high-level, abstract specifications. There's no way yet that I know of where we can synthesize the program from the specification although I am aware of research in that regard. However we can still gain the benefit of well-defined invariants and pre/post-conditions that we can use in testing our implementation. For now your implementation will be separate from your spec but you gain insights from the spec you would not otherwise if you had only written code.
update as to whether it is an efficient use of time to use a model checker or automated theorem prover... Well I think the reason for their invention was to specifically to handle the tedious task of proofs in formal maths. Some operations are tedious and mechanical and computers are better suited to the task than humans.
One area I find interesting is languages with dependent type systems like Agda and Idris. It seems like we're not too far away from being able to model and prove our specifications directly in the type system alongside the program that implements it.