21–30 of 31 posts
Two more: https://arxiv.org/abs/1907.07794 https://arxiv.org/pdf/1904.03241.pdf
And another https://arxiv.org/pdf/1608.02644.pdf I'd really love to see someone like Deepmind get a hold of this. They are perfectly placed to apply a lot of resources to it and it's right in their wheelhouse. Don't know how to contact them about it though.
Two more: https://arxiv.org/abs/1907.07794 https://arxiv.org/pdf/1904.03241.pdf
There has been a lot of work like this popping up in the past year. I think it's somewhat promising, but for ML for ITPs to really become useful, I think the models need to better take into account semantic information about terms and types and not just tactics. And this is not easy, because Coq's logic is higher-order and dependently typed, and most work in ML for PL deals with much simpler logics. Still, anything t…
Have you thought an interactive site where people could learn coq writing proofs? Something very similar to https://projecteuler.net/ . You could get thousands of failed proofs very fast.
Is anyone aware of a proof system that can do independence proofs over a set of axioms?
However, at the moment I'm a bit enamored with Metamath [1]. It's basically a tiny system that just performs formal substitution. Everything else, including propositional calculus, predicate logic, and ZFC set theory is encoded within the language, rather than the implementation. I.e. it's a metalogic that only knows about simple substitution. That way one can easily investigate other logics and axiom systems, e.g. they have stuff for intuitionist logics, orthomodular lattice models, you name it.
Anyway, the project already has a pretty substantial collection of theorems, including a lot of analysis, topology, algebra and even QM. The cool thing is that you can easily dig up how the high level proofs trace back to the fundamental axioms, and there's no fancy math happening in the metalogic at all.
Super cool stuff.
Is anyone aware of a proof system that can do independence proofs over a set of axioms?
All of them? I don't understand why you think existing systems are not able to handle independence proofs. You embed your model in the logic of the system, and this approach works for all proof assistants.
Earlier quoted context omitted.
Idea for getting "almost correct" proofs: Take a big Coq project like CompCert or whatever. Search the version control history for commits with small changes to definitions. These very likely come with corresponding changes to proofs as well. Now apply only the code changes but not the proof changes: You get a state with "almost correct" proofs and as a bonus known "ground truth" proofs as well.
This is a really interesting idea. In some sense, you can say a proof script is "almost correct" if it proves a slightly different theorem. I suspect the one difficulty there would be finding such incremental changes on Github. It was surprisingly difficult to find small changes to specifications in Git history for a different project that I did. Too many large commits and too much history revision, so you often lose…
Earlier quoted context omitted.
Can you explain what parts of the TLA+ stuff you can express in Prolog and why you think that might be better (or equally good)? It's true that modeling languages all have something in common with Prolog, but do you think that proofs about a similar Prolog version would be nicer than in TLA+?
I don't know if it's better or nicer. "I am but an egg." Here is Lecture 4 of Lamport's course: https://lamport.azurewebsites.net/video/video4.html TLA+ source code: EXTENDS Integers VARIABLES small, big TypeOK == /\ small \in 0..3 /\ big \in 0..5 Init == /\ big = 0 /\ small = 0 FillSmall == /\ small' = 3 /\ big' = big FillBig == /\ big' = 5 /\ small' = small EmptySmall == /\ small' = 0 /\ big' = big EmptyBig == /\ b…
If you're only interested in the specification part of TLA+ but in proofs, that's great. But then it's not fair to claim that you can do everything in Prolog that TLA+ does.
Earlier quoted context omitted.
I don't know if it's better or nicer. "I am but an egg." Here is Lecture 4 of Lamport's course: https://lamport.azurewebsites.net/video/video4.html TLA+ source code: EXTENDS Integers VARIABLES small, big TypeOK == /\ small \in 0..3 /\ big \in 0..5 Init == /\ big = 0 /\ small = 0 FillSmall == /\ small' = 3 /\ big' = big FillBig == /\ big' = 5 /\ small' = small EmptySmall == /\ small' = 0 /\ big' = big EmptyBig == /\ b…
This is very neat. It shows that Prolog is very close to being the holy grail of an executable specification language. But my question was about verification: TLA+ is not just used for modeling but also for proving stuff about the models. Do you have anything similar for Prolog? If yes, I would love to use it :-) If you're only interested in the specification part of TLA+ but in proofs, that's great. But then it's no…
Cheers!
> Do you have anything similar for Prolog?
Well, what you think of "Formal Methods: A First Introduction using Prolog to specify Programming Language Semantics"? https://homepage.cs.uri.edu/faculty/hamel/pubs/fcs16.pdf
Abstract
> An important fundamental idea in formal methods is that programs are mathematical objects one can reason about. Here we introduce students and developers to these ideas in the context of formal programming language semantics. We use first-order Horn clause logic as implemented by Prolog both as a specification and a proof scripting language. A module we have written facilitates using Prolog as a proof assistant and insures that Prolog implements a sound logic. In order to illustrate our approach we specify the semantics of a small functional language and demonstrate various proof approaches and styles.
I just found this the other day and it seems promising.
> it's not fair to claim that you can do everything in Prolog that TLA+ does.
A claim I didn't make. "So far", I said, and, "I'm not to far into it yet" (sic). :-)
(Although it's trivially true because of Turing completeness, eh?)
I have great respect for Lamport. I would hate to be unfair to him.
Earlier quoted context omitted.
This is very neat. It shows that Prolog is very close to being the holy grail of an executable specification language. But my question was about verification: TLA+ is not just used for modeling but also for proving stuff about the models. Do you have anything similar for Prolog? If yes, I would love to use it :-) If you're only interested in the specification part of TLA+ but in proofs, that's great. But then it's no…
> This is very neat. Cheers! > Do you have anything similar for Prolog? Well, what you think of "Formal Methods: A First Introduction using Prolog to specify Programming Language Semantics"? https://homepage.cs.uri.edu/faculty/hamel/pubs/fcs16.pdf Abstract > An important fundamental idea in formal methods is that programs are mathematical objects one can reason about. Here we introduce students and developers to thes…
Still, I'd like to see more work along these lines.