Comment by nickpsecurity | Hacker News Reader

Comment by nickpsecurity | Hacker News Reader

Parent Full thread

Your TLA+ comment isn't relevant to this discussion and seems to only promote TLA+. The topic is verification of compilers or imperative programs in C language. I don't know of anyone using TLA+ for that or advocating for it. It's mainly used as a lightweight approach in protocol verification. So, distributed apps not C code or compilers.

Now, Coq has plenty of history in certified programming and compilation. There exists formalisms and models of most pieces of the puzzle. There are worked examples of certified compilers whose details and sometimes source are available for re-use. There's even already a verified C compiler other works are building on. It was used in EAL7-class JavaCard interpreters, database structures I believe, web services, and so on. Even outputs to robust Ocaml code. People needing to learn this stuff even have free books like Chlipala's:

http://adam.chlipala.net/cpdt/

So, anyone trying to specify or formally verify compilers or algorithms have plenty of reason to choose Coq. It's actually one of the best tools for the job with HOL or Isabelle the other style. Field kind of diverges doing parallel work with them in imperative verification. Coq is possibly easier to use and seems to have more prior work to draw on in this. So, it's either the best or one of best tools for the job.

TLA+ is for totally different jobs. Not relevant here.

As I said in another comment, stories like this make people interested in formal methods, and Coq, IMO, would be daunting for most beginners. TLA+ is a good, beginner-friendly entry point to formal methods (and you can slowly progress from specification to model-checking and only then proofs), even if you later choose to move to dependent-type approaches and tools like Coq or F*.

> TLA+ is for totally different jobs. Not relevant here.

I beg to differ. TLA+ is commonly (as far as the word "commonly" can be used when formal methods are discussed) used to specify and verify programs in C or any other language.

It is true that Coq has been used to verify compilers more than TLA+, while TLA+ has been used to verify algorithms (esp. concurrent/distributed) more than Coq, but the reason is not because neither could do the other's job, but because of their respective progeny. Coq (as all type-theory tools) is closely associated with PL-theory people, who tend to be more attracted to compilers, while TLA+ originated from the software-verification world (mostly Pnueli's temporal logic), and created and promoted by Leslie Lamport, most certainly an "algorithms" (specifically distributed/concurrent) guy rather than a "PL" guy.

BTW, Isabelle is one of the proof engines used by the TLA+ proof system.

" stories like this make people interested in formal methods, and Coq, IMO, would be daunting for most beginners. TLA+ is a good, beginner-friendly entry point to formal methods (and you can slowly progress from specification to model-checking and only then proofs), even if you later choose to move to dependent-type approaches and tools like Coq or F*."

TLA+ is an easier intro to verification. However, the verification of C programs to any strong degree will require tools like Coq, possibly esoterica like separation logic, tough specs, tough proofs, and so on. There's no easy route for it for beginners except to straight up learn the necessary knowledge with Chlipala's book, Software Foundations, or something similar. Then plenty of practice and study of how successful work was done.

There's a reason we celebrate every time someone comes close to specifying or verifying a significant chunk of C language. It's because it's Just That Hard (TM). ;)

"I beg to differ. TLA+ is commonly (as far as the word "commonly" can be used when formal methods are discussed) used to specify and verify programs in C or any other language."

Hmm. Interesting. I should probably do another survey of TLA+ to see what uses it's had in sequential, low-level algorithms like the OP post is on. May be more going on than I was previously aware. All the top results are using Coq and Isabelle/HOL, though.

> There's no easy route for it for beginners

And if this post had appeared on a Coq forum, a verification forum or even LtU, I would have said nothing. However, as this is HN, and there are probably many beginners reading this, I thought it very relevant to point out a more beginner-friendly tool as a foray into this interesting subject.

> what uses it's had in sequential, low-level algorithms

This is a fairly recent paper that describes a tool that translates C to TLA+ for verification: http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MLBHB-ftscs15... It works for concurrent C programs as well as sequential ones.

This is an old (old) spec by Lamport of the Win32 Threads API: http://research.microsoft.com/en-us/um/people/lamport/tla/th...

And again, the choice of TLA+/Coq often has much more to do with the community the author belongs to (PL/conc-dist algorithms) rather than some specific strengths of the tool.

Appreciate the paper as I didn't have that interesting work. Once again, though, they're focused on the details of concurrent (eg protocol-like) work instead of verifying concrete, sequential programs. They claim in the paper to be able to prove absence of runtime errors but don't give much detail. They also aim to do more on that leveraging Frama-C but again no detail. So, your example shows it a work in progress for TLA+ rather than work done several times over as in Coq or Isabelle work.

It does support the use of TLA+ for some aspects of C verification or specification along with integrating into the right tool (Frama-C). I'll probably do the re-survey on TLA+ use I mentioned earlier due to this paper.

I've been wondering for a while, and since this thread seems to have attracted people who may have answers…

Can you (or anyone) provide any insight as to why ACL2 doesn't get mentioned much in discussions of formal methods? I'm interested in formal methods and ACL2 seems like a nice tool, but at least on HN all I usually see is Coq this and Coq that, with occasional mentions of TLA+ and Isabelle.

I'm not sure why it doesn't get mentioned a lot. I do know that both LISP and best use of ACL2 (i.e. hardware verification) both get little mention in general. A variant of one to do the other should be similar.

The best work I've seen in ACL2 comes from Rockwell-Collins and their SHADE verification suite. They've verified raw hardware, microcode, processor ISA, security policies, crypto systems... you name it. They give plenty of detail in their papers in how they do that albeit some are paywalled. The resulting AAMP7G processor is used in commercial applications needing reliability and security.

I haven't done a straight survey on ACL2 in a while, though. Might be worth a reader doing and posting in case something interesting was overlooked. Rockwell's stuff seems to be best use of it, though.

Not sure if you'll see this, but I did run across a preprint with a few Rockwell authors that might be of interest, "Development of a Translator from LLVM to ACL2" (http://arxiv.org/abs/1406.1566)

That's interesting work. Hardin is the name that was on the other ones. No surprise they dragged LLVM intermediate form into ACL2 to leverage their prior work. Good that it's fast but I'm more interested in what analysis they can do and how easily. Wish it had more of that.

Still added it to my collection as it might come in handy for future ACL2 work. :)

> Your TLA+ comment isn't relevant to this discussion and seems to only promote TLA+.

pron has this habit of being negative and dismissive towards functional programming and related things, recommending non-FP alternatives instead. Which is fine, only that sometimes he's too trigger happy and just gives unsolicited advice without any build up or with weak topical relevance. Like here.

I am not dismissive towards Coq (how can anyone be?), and my advice is neither less solicited nor less relevant than many other HN comments.

But you are right that I sometimes try to correct what I see as a (strange) imbalance here on HN (which reflects neither the prevailing opinions in academia nor in the industry) regarding PFP and type theory. People unfamiliar with the topic might get the impression that PFP+type-theory is either the only or the most prevalent technique for software verification (or software correctness in general), while neither is the case. In exchange, I get to be the lucky target of various ad hominem attacks, so I guess I've earned my right to speak up :)

The phrase "ad hominem" has become really watered-out.

I noticed along with no supporting evidence presented in relevancy for this topic. Hence my comment. ;)

Reply on news.ycombinator.com