ACL2 is an alternative that strives to strike a balance between interaction and automation.
- It is more automated than any of the interactive theorem provers including Isabelle/HOL, Coq, etc.
- Its authors received the ACM software system award in 2005.
-It is used in commercial products since several years in companies including AMD, Centaur , Rockwell Collins, etc. There is a not-so comprehensive but yet impressive list of applications here:
http://www.cs.utexas.edu/users/moore/publications/acl2-paper...
- Also, since the language is a subset of Common-lisp, any one who knows a bit of programming can very quickly start using ACL2. One does not need to learn type theory/logical formalism to start using it. It has an eclipse plugin that is used by first and second year undergraduate students (http://acl2s.ccs.neu.edu/acl2s/doc/).
I would guess an database of previously proved lemmas for all the used libraries would help, so that you don't have to recompute everything.
[0] quickcheck is an awesome library that generates unit-tests for specified properties (like: "for all lists s: length(sort(s)) = length(s)", i would then just generate a few hundred lists and check whether the property got violated)
Yes, kind of. For certain values of "similar ease" and "Haskell". AFAIK Agda is pretty much Haskell, but its proving part is not all that automatic. On the other hand, Isabelle has a lot of proof automation (and includes an implementation of QuickCheck that it applies automatically to every property you state when you start proving it!), but its own variant of functional programming is not exactly Haskell. I think you can extract Haskell programs from it, though.
> I would guess an database of previously proved lemmas for all the used libraries would help
It may help, but it may also confuse the proof search if it gets lost in a sea of irrelevant lemmas. Which is what I was trying to say above, I never said anything about recomputing stuff.
> Yes, this should be possible, and it is possible.
Regardless of the formal tool you use, be it Coq, Idris, TLA+ or Isabelle, proving what you need proving most -- the non-trivial stuff -- is never quick and easy. The reason it's hard to prove non-trivial algorithms correct is because it's hard to write non-trivial algorithms correctly. Temporal logic, HOL, SMT, dependent types, model checking, abstract interpretation -- they're all useful tools, but in the end, to make the utmost of formal methods, and understand the difficulties and possibilities, one must first understand the nature of algorithms and how they work, and this is always the same, regardless of the particular formalism used. Personally, I've found TLA+ to best isolate the core of the issue with as few distractions as possible, and others may find other formalisms to better suit how they think, but the essential problem is always the same.
It is true, however, that some formal tools impose more accidental complexity than others. The ones that are most refined are those that are used by real engineers on large real-world software every day, like SCADE, TLA+, SPARK etc., while things like Coq and Agda are mostly aimed at researchers and designed to let them explore new ideas.
In practice, the industry uses automated formal methods -- SMT solvers and model checkers -- almost exclusively, with interactive deductive proof used to tie results together or to fill in a few missing gaps. Interactive theorem proving is currently too costly as a primary tool for use in real-world software, in all but the most high-assurance settings.
> Look up SEL4 and CompCert for a start.
seL4 and CompCert -- while great achievements -- are neither good examples of formal methods, nor are they particularly encouraging. For one, they were academic projects that took world experts years of effort for what amounts to very small software as far as industry software goes (comparable to a ~10KLOC C program). For another, the kind of verification they required is what's known as "end-to-end", namely global correctness properties are proven all the way down to machine code. This level of correctness is unnecessary for 99.99% of software; perhaps even for no software at all.
Much better examples of the use of formal methods in industry include the use of SCADE to write thousands of safety-critical, hard realtime software every year; the use of Z and Ada SPARK by AltranUK to write large, complex defense software; the use of SPIN and other model checkers to find flaws in hardware designs, the use of B-Method in the railway sector, and the use of TLA+ at Amazon, Oracle and other companies for complex server-side services.
> proving what you need proving most -- the non-trivial stuff -- is never quick and easy
The OP asked for proving "many things" quickly. You can prove many things in Isabelle by writing something like "by induction n. sledgehammer" and waiting for the automated machinery to do the rest. This doesn't suffice for everything, of course. But it's good enough for "many things", including stuff that would take a lot more work in Coq.
> seL4 and CompCert -- while great achievements -- are neither good examples of formal methods
The OP said they are not aware of any "formal proofs for programs". These are some examples. Many of the other things you mention use formal models, but not necessarily formal end-to-end proofs.
> "end-to-end", namely global correctness properties are proven all the way down to machine code. This level of correctness is unnecessary for 99.99% of software; perhaps even for no software at all.
Compiler bugs are a thing. At Airbus, the generated assembly code is inspected manually for bugs introduced by the compiler (which is untrusted, and takes input C code generated by SCADE's untrusted code generator). You think that's useless voodoo?
> formal methods in industry include the use of SCADE
SCADE is great, and it's "formal methods" in the sense that you write your program as a formal model with clear semantics that can be reasoned about. But it's not the kind of proof the OP asked about, I think.
No, but I also think it's just not worth the effort for 99.99% of software. It's neat that it can be done when absolutely necessary, but that's not where most of the benefit of formal methods can be had. Also, you don't need many certified compilers, so the techniques used to construct them need not be scalable.
> SCADE is great, and it's "formal methods" in the sense that you write your program as a formal model with clear semantics that can be reasoned about. But it's not the kind of proof the OP asked about, I think.
Well, they wrote "I would image that certain languages are easier to prove (haskell vs C)", and SCADE is easier to formally reason about -- be it with a model checker, static analysis or deductive proofs -- than Haskell. Usually, languages with very simple semantics are easier to reason about either automatically, manually or semi-automatically, and the languages that are used in the industry in formal methods (except static analysis) -- even if the formal methods used aren't deductive because that's just too costly -- are those that really are "easiest to prove".
It is. That's why Coq is a pure functional language, rather more like Haskell than like C.
> and with the right tooling it should be able to prove many things quickly
Yes, this should be possible, and it is possible.
If you mean you want it to be automated: Isabelle/HOL has more automation than Coq. For many simple things, it suffices to tell Isabelle, essentially, to perform induction on a given variable and from that to try to find a proof automatically. It builds on several external provers to implement this.
What is difficult is for the system to know which existing lemmas to reuse and how to combine them. It's a bit like your math homework, except that these systems know more lemmas (i.e., have a larger search space) and are not always good at ranking them by relevance.
> right now i don't see formal proofs of programs at all (i only hear some rumours that some companies use it at some small scale)
Look up SEL4 and CompCert for a start.