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).
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.
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.
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).
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).
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.
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.
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.
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...
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/