Home » forums » LtU Forum

Proof formats

During the development of a language which allows formal verification I have experimented a lot with proof formats. First I have started with a proof language with tactics similar to Isabelle/HOL and Coq. But then I realized that such proofs are fairly difficult to read. In order to understand a proof one often writes down the state of the proof engine at intermediate positions of the tactics. Then I have introduced proof procedures stimulated by some examples in the dafny language.

Up to now I think that tactics are not appropriate to write down and document proofs. In the posts Boolean lattices, Predicates as sets and Complete lattices and closure systems I have used a proof format which I think is good to write down and document proofs.

Any opinions, remarks etc. are welcome.

By hbrandl at 2012-09-25 17:43 | LtU Forum | previous forum topic | next forum topic | other blogs | 3492 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

I think you're doing a lot

I think you're doing a lot of neat stuff, here. I love the formatting of proofs into features.

I think, for presenting error messages and for self-documentation, it might be best if you enabled labeling features (perhaps at a sub-feature level, e.g. using a `label` directive, or via a more generic annotations concept `anno label ...`).

Does your proof system have any support for linear or substructural logics?

By dmbarbour at Wed, 2012-09-26 17:45 | login or register to post comments

Labels are already used in

Labels are already used in the proofs. Their primary purpose is for documentation and cross references (which are only for the human reader). If you look into the proofs you will find at the start of each assertion an optional label of the form "label_name:". Maybe you are talking about something different?

I don't understand what you mean by linear or substructural logic in this context.

By hbrandl at Wed, 2012-09-26 18:14 | login or register to post comments

Linear logic could, for

Linear logic could, for example, provide a proof that every argument to a function is used in computing the result, or that at most one argument is used. It's a great tool for modeling the physical (communication, performance, resource) aspects of computation. E.g. by modeling partitions, one could enforce that an algorithm only uses resources that are locally available, and that moving resources (or moving partitions) shifts the availability properties.

LL is probably the one thing I most miss in popular proof systems, though there are layered techniques to express it with a rich enough system.

The labels are obvious now that I know for what I'm looking. I guess `lemma_1:` didn't strike me as very useful documentation.

By dmbarbour at Wed, 2012-09-26 18:56 | login or register to post comments

Linear logic

I am afraid that this is currently beyond the scope of what I am doing. I try to define a general purpose language which allows specification, implementation and verfication of arbitrary (including concurrent) programs. This goal is already quite ambitious.

By hbrandl at Wed, 2012-09-26 19:14 | login or register to post comments

Linear logic within the language

Of course you can model linear logic within the language. Since the compiler models classic logic in order to verify the correctness of the code, it is possible write a program which models linear logic. But linear logic will probably not builtin into the compiler/verifier.

By hbrandl at Thu, 2012-09-27 14:47 | login or register to post comments