A Lisp Way to Type Theory and Formal Proofs (2017) [pdf] | Hacker News Reader

A Lisp Way to Type Theory and Formal Proofs (2017) [pdf]

european-lisp-symposium.org

183 pointspmoriarty16 comments

Looks neat but no mention of ACL2 in project about LISP and proving? Come on, now! I wonder if the author investigated it. If so, why not use it or improve it. So far, it's one of most successful in terms of industrial use with SPIN being other one (TLA+ doing similar stuff now).

https://www.cs.utexas.edu/users/moore/acl2/

Far as TCB, Jared Davis, who used ACL2 on x86 processors, built a self-verifying prover for a logic going in ACL2's direction. It was verified to assembly using Magnus Myreen's techniques.

https://www.cs.utexas.edu/~jared/milawa/Web/

Bootstrapping theorem-proving, that's awesome!

SPIN and TLA+ aren't proof assistants at all - they're model checkers, that is, they simulate a model some number of times and check that the desired properties hold in all explored states. Obviously this means they're not providing a guarantee that the properties hold for all states: there's no proof, only evidence. This doesn't mean they're useless, but it does mean they're not proof assistants.

ACL2 is a proof assistant, at least, but it's not based in type theory, so that's probably why they didn't use or improve it. ACL2 looks like it's specifically intended to aid in proving theorems about models of software systems, as well, which probably makes its logic system a bit clunky to use when expressing theorems about mathematical structures.

I meant most successful uses of verification tech, not proof, for SPIN. I shoudve worded that better. There is a version of it in a proof assistant called Favela if I recall. TLA+ has a proof system (TLAPS) and a model checker. Finally, if state and transitions are small, then a model-checker can give you similar assurance as a proof by essentially checking everything. These days, that's rarely the case, though.

ACL2 was designed for real hardware and software. That's what many use it for. Rockwell-Collins builds CPU's, separation kernels, and low-level software for NSA with it. I agree author maybe dodged cuz it's not type theory.

Model checking is a proof method. If all possible states are explored, that is a pfoof (Proof by exhaustion).

It's not exactly proof by exhaustion, as model checkers don't actually check all assignments, even explicit-state model checkers (because even in finite state cases, verified propositions are about infinite behaviors; you often model-check propositions much more elaborate than "X never happens in any state"), and algorithms like DPLL for SAT model-checking don't even do explicit state visits. Rather, it is a proof in the model theory of the logic.

1. TLA+ is a language. TLA+ specifications can be verified with either a model checker or a proof assistant. TLA+'s proof language is one of the most elegant I've seen.

2. A model checker most certainly provides 100% guarantees. This is why it's called a model-checker: it checks that a system's Kripke structure is a model[1] (i.e. a satisfying assignment) for a formula. It's just that model checkers often fail to check infinite state spaces and so people often check a finite instance of a specification. While model checkers have occasionally found errors in (informal but peer-reviewed) "proofs", I am not aware of any cases to the converse (obviously, when a finite instance was used for an infinite-state system). Both model checkers and deductive proofs have limitations and are generally complementary, but currently model checkers are considered to be much more scalable.

Also, model checkers don't "simulate a model some number of times." (the model-checking algorithm for temporal logic won the Turing award for its inventors). Even in finite state cases, model checkers check temporal formulas on infinite behaviors (e.g. that every request is eventually matched by a response).

[1]: https://en.wikipedia.org/wiki/Model_theory

Some model checkers are bounded model checkers, for example CBMC, a bounded model checker for C. In practice this sometimes means they only unroll loops a certain number of times, so they might miss assertion violations occurring in later iterations of a loop. You're right though that there are model checkers that are not bounded and these do provide guarantees.

Yes, as their name suggests, bounded model checkers check bounded models rather than models. In the literature, bounded models are virtually never mentioned unqualified (i.e., a bounded model checking algorithm won't be presented as a model checking algorithm).

Hello, I don't have the paper right now but I doubt I don't cite ACL2 since I have been a user for a long time... I'll double-check but indeed I have mostly kept the discussion around type theory...

I was mainly commenting so people interested in LISP verification knew to check it out to make sure they reap any benefits from a mature tool. I'd have been shocked if you hadn't heard of it. I was just a little confused since it's usually mentioned as prior work or something. Glad you're already benefiting from it.

Yeah, focusing on stuff closer to your direction of type theory makes sense. Thanks for writing up your work and good luck on your project.

The book[0] mentioned is excellent if you are interested in this kind of thing. It is available on Kindle too.

[0] https://www.cambridge.org/core/books/type-theory-and-formal-...

Author here. If you are interested I talked about type theory at euroclojure'16. The video is there: https://m.youtube.com/watch?v=5YTCY7wm0Nw

... And it's not really clojure-specific except if you want to try LaTTe:

https://github.com/latte-central/LaTTe

Oh, Dr Peschanski. If you're interested he was also into random trees https://github.com/fredokun/arbogen

If you're interested... A tutorial about this topic... It's clojurescript in the browser but I think the algorithmic explanations do not require any lisp knowledge...

(Edit missing link)

https://github.com/fredokun/talk-clojureD-2018/blob/master/R...

Hello, didn't see that talk, thanks

Reply on news.ycombinator.com