Arend: Theorem Prover Based on Homotopy Type Theory by JetBrains
arend-lang.github.io
arend-lang.github.io
https://www.oracle.com/database/technologies/developer-tools...
I did a whole MSc in Formal Methods about a decade ago, and I think abstract interpretation, model checking and axiomatic specifications are ready for prime time now. Exotic type systems and theorem provers are still a bit costly to use, but have achieved some spectacular successes like seL4.
I guess JetBrains wants to be in this space once things mature.
Most, not all, formal methods tools are a tire fire of incoherent UX, bespoke Byzantine runtime requirements, and scattered piecemeal documentation & tutorials.
Which makes complete sense when you consider where they originate, what they're typically used for, how they're maintained, and who their subset of end users are. You have to reeeeaaaalllly need to reach for one of these tools to put up with how bad they are, and the population of developers who have that need is significantly smaller than the population who could derive some value & benefit from the methods were they not also unnecessarily painful to use on top of their already being conceptually challenging for the uninitiated.
Their niche status becomes self-perpetuating. A company like JetBrains making a move like this might stand a chance of breaking the logjam.
A language (like Dafny?) with garbage collection plus the techniques behind those two would make for a very powerful toolset.
If you try Idris, although mostly people are just using it with text editor with simple plug-ins, the auto-completion is incredible: you can auto complete a whole paragraph of code based on the signature rather than just a method, and then you can just do some minor changes.
> The project started incidentally in 2012 when one of the teams at JetBrains was developing a collaborative real-time editor based on operational transformation (OT). With the help of Coq proof assistant, a suitable OT algorithm was developed and validated, but the interest in automated proof checking and formal verification as applied to real-world tasks led to a creation of a separate research group. In 2015 the group switched over to the development of the experimental HoTT language.
However I cannot find a precise reference for the chosen type theory.
E.g., is univalence a theorem in their type theory? I presume it is given that they say their language has "syntax similar to cubical type theory" but I could not say for sure.
What I'm looking for is a reference containing the actual typing rules, like this one for Coq: https://coq.inria.fr/refman/language/cic.html#typing-rules
rather than the syntax of the language used for building these terms.
For example, they emphasise that function extensionality is a theorem here: https://arend-lang.github.io/about/arend-features (not true in CIC).
It would just be nice to see a list of the rules.
Still I don't want to get hung up on this; the rules must exist somewhere and presumably will become more discoverable. The project looks superb.
I always believe this field would be very useful and evolving steadily in the industry. It just doesn't attract eyeballs like machine learning and blockchains.
https://leanprover.github.io/about/ https://github.com/leanprover/vscode-lean
... yet. The next AI Winter is right around the corner. While there has been seriously amazing work coming out of ML, in industry there is an insane amount of resources being put into completely BS ML systems. Outside of FAANG there are many "fancy" ML projects in industry that are just continually accruing massive technical debt, and for no good reason. The number of deep neural networks being used for problems that can be solved with radically much more simple (and easier to debug and maintain) techniques is astounding. Right now there is a boom in complex and fragile a systems made by teams of PhD in non-engineering fields that don't know anything about system or software design.
In a few years these complex systems will need to be maintained and fixed and it will quickly become apparent that the vast majority of these projects are a huge business liability with minimal financial or engineering benefit. Expect a huge back lash against predictions coming from complex, non-interpretable linear algebra heaps.
The pendulum will swing back, and likely pretty hard (as always probably too hard). I'm not sure theorem provers will be the winner, but the general class of understandable, predicable, and explainable things will become more popular. It is quite possible that "my tool proves things are stable and work" will be a big sell in the next wave of tech.
It would be fun in a TheDailyWTF way :)
Stories of AI Failure and How to Avoid Similar AI Fails in 2019 https://www.lexalytics.com/lexablog/stories-ai-failure-avoid...
How IBM Watson Overpromised and Underdelivered on AI Health Care https://spectrum.ieee.org/biomedical/diagnostics/how-ibm-wat...
Automakers Are Rethinking the Timetable for Fully Autonomous Cars https://www.designnews.com/electronics-test/automakers-are-r...
As an aside, my worry with AI/ML is that we’re creating these giant, un-debuggable systems that can’t be fixed when specific problems arise. Every time I see complaints about YouTube/Facebook/<some other company> giving nonsense recommendations to people I think “How would they even fix that? Do they even know how their recommendation systems work?”.
One of the great things about software is that when something is broken, you can go right in there and fix it. With ML, I can imagine getting to a point where our only option is to take the black-box we’ve created to therapy and hope for the best.... :)
https://ncatlab.org/nlab/show/Homotopy+Type+Theory+--+Unival...
- Use HoTT or any other type theory as a logic / foundation of math.
- Use Hoare logic to reason about programs, using your logic / foundation of math to deal with inferences that are not given by the rules of your Hoare logic, i.e. for Hoare's "Rule of Consequence".
There are several ways of connecting the two. One is Hoare type theory [1]. Another is using Characteristic Formulae [2, 3].
[1] G. A. Delbianco, A. Nanevski, Hoare-Style Reasoning with (Algebraic) Continuations.
[2] L. Aceto, A. Ingolfsdottir, Characteristic Formulae: From Automata to Logic.
[3] A. Chargueraud, Formal Software Verification Through Characteristic Formulae.
The documentation for \lemma (https://arend-lang.github.io/documentation/language-referenc...) suggests that you would just write Prop-typed functions, which is very tedious to do manually and even with automation is IMHO inferior to Coq-style tactics, which are themselves often inferior to Isabelle's Isar-style proofs.
\lemma op_is_revertible (C : PreCat) : op (op C) = C =>
path ( \lam i => \new PreCat {
| Ob => C.Ob
| Hom => C.Hom
| id => C.id
| o => C.o
| l_unit => C.l_unit
| r_unit => C.r_unit
| assoc => \lam {a} {b} {c} {d} f g h => (inv_inv (C.assoc f g h) @ i)
}
)
destruct C; auto using assoc, inv_inv.
Not a lot of languages have higher-inductive types which is the main advertised feature here. At least they're missing in Isabelle and Coq.
That's also orthogonal to the matter of automation/metaprogramming, which, from the lack of mention, doesn't seem to be their focus right now. There doesn't seem to be anything fundamentally in the way of Coq-style tactics either if they really wanted to build that on top of what is presented here.
Unless you desperately need exactly this kind of fancy logic, if you actually want to get stuff done, you would choose a different system. That's not great if they are interested in wide adoption.
Better tools are still needed, so people really should be building more systems of this kind.
Actual citation from the paper or some other source needed.
Relevant-ish citations from the paper:
1. "Coq uses interactive tactics to prove goals, which is veryconvenient, but may lead to large proof scripts in case onedoes ad-hoc proofs. But Coq also has the tools to make theproofs concise, provided one works in a fixed domain, andcreates the necessary abstractions."
2. "In [50] Wadler states“Proofs in Coq require an interactiveenvironment to be understood, while proofs in Agda canbe read on the page.”, while this is true for the languagesthemselves, but Proviola [49] can alleviate this problem ofCoq, by recording the proof state after each tactic execution,and producing an html document with the proof state addedfor each tactic. F* does not have this problem, as the proofterms do not appear either in the source, or during proving.Whether it is easier to read complete proof terms, or thereplay of a step by step creation of a proof term is dependentof the task at hand, but the author thinks, that it is morestraightforward to create scripts step by step in Coq, thoughit does require discipline on the programmer’s part, so as tonot create a write-only script"
Are you basing your very wide claim on one of these that don't say what you're saying, or did I overlook one?
Anyway, there's CompCert (http://compcert.inria.fr/) and Iris (https://iris-project.org/) and Kami (http://plv.csail.mit.edu/kami/papers/icfp17.pdf) and many other projects of non-toy size implemented in Coq, so I don't quite know what else to say to convince you. Sure, tactic scripts can be hard to read and next to impossible to skim. The same goes for direct proof terms.
> Better tools are still needed
Agreed.
This doesn't inspire confidence, considering this author is also the most familiar with Coq of the three. He also somehow claims that Coq is stable, which I can only take to mean that it won't crash rather than that it largely preserves backwards compatibility given his difficulties. If we can't rely on some measure of backwards compatibility so we can build on stable libraries, theorem proving simple won't scale any more than programming of any kind won't scale in the same circumstances.
The number of lines of code required for the second task also doesn't inspire confidence that theorem proving with Coq will scale.
So I frankly can't see any reason to think that Coq even with tactics is a viable approach to real world verification beyond exploratory toy examples. No doubt we have different goals in mind when it comes to verification/theorem proving, which is why you think Coq is suitable and I do not.
The question is not whether tactics are useful in some cases, the question how robust and stable they are, because if older libraries employing tactics no longer work, this is not a robust foundation for long-term verification efforts.
I'm not going to argue about a paper written by someone whose proficiency in Coq I cannot judge with someone who doesn't seem to know anything about Coq except having read this one paper.
F* looks very good in this comparison, which is great. As you wrote above, we need better tools, and F* is getting there. Simple things can be tedious in Coq, and F* 's automation should help there.
Regarding compatibility: neither Coq nor Agda used to have much of it; nowadays Coq is maintained together with a large set of community projects, and code is much more stable. Still tons to do.
I've learned about \lemma and \property and HoTT precategories and univalent categories not so long ago. Now I'm planning to rewrite all of this from scratch
Is this just for programming language research? What kind of projects would you want to use this language for?
The answer to that is that there are no good tools and no universally accepted common notation that is amendable to automatic proof checking yet. Those are problems that projects like this want to solve.
I applaud the effort really; it's hard work, and people tend to ask more critical questions ("What is it good for?" "Theorem proving is for academics only") than for any other type of program.
E.g.: Is the hope to make something all mathematicians will eventually use? Is it targeted at a relatively narrow mathematical field? Is the audience instead programmers looking to prove things about algorithms they're working on?
'Understand' is a big word. I've played around with Idris (which is a Haskell-like programming language that supports Homotopy type theory as well). I have a grasp of the underlying mathematics but don't really understand the stuff deeply.
Yes, I went on a bit of a rant and totally ignored your (totally reasonable) question. Theorem proving and proof checking are quite niche, both within computer science and mathematics. In computer science, the idea is that you can formally prove the correctness of computer programs to avoid software failures and have very robust programs. In mathematics, the ideal is to have
1. A universal language for proofs
2. A database of computer-verified results
3. Easy verification of new results
The advantage of a "safety net" has a big fight on his hands against the big disadvantage of "who's going to maintain this shit when that rock-star theorem guy is gone?". Or the theorem guys are very expensive in the first place, so it's cheaper or easier to hire multiple people who have to use unit tests like everybody else.
So eventually if - a language but more importantly - an ecosystem like that will get leverage, every existing ecosystem can slowly fade into that and develop further in this path.
At the end (almost all) programmers are going to write proofs, because this is what works in scale.
Please correct me if I am wrong!
We're currently the early explorers of a field, mostly composed practices & tips and tricks that we think help but can't be sure. We're like barber-surgeons before it turned into a true profession.
I believe we have plenty of examples today of “we can’t fire this employee because a few years ago we made a mistake of that hire and now they are the only ones who know how that pile of shit works”.
At least with theorem provers the transparent knowledge of the broken systems can be formalized.
At this point, I think the rockstar theorem guy would not be working on some proprietary business logic that needs to be maintained wholly in-house. He'd be in charge of more critical infrastructure in widespread use. Kernels, SSL libraries, optimizing compilers; that sort of thing.
As for who should hire him? I'd hope one of the big tech companies would want a project like this.
That's because the field is still in an exploratory and research phase. Unless you're in an industry where correctness is the most important criteria or involved in research into this stuff, your average programmer isn't going to be using any of this. It's still too early, but that doesn't mean it's a waste of time.
For most of the cases where formally verifying _designs_ is important (most of the industry), formal specification languages are 1) not actually that hard to learn, and 2) exist distinct from the code, so you can throw them all out if you really need to and go back to flying blind.
1. As a formalized specification language that allows you to engage in a dialog with the computer about what properties are entailed by such a specification. For example there is a team at Amazon that makes use of the language TLA+ to formally specify some AWS systems and use the computer to derive and check insights about those systems. This focus solely on the specification and ignores the code implementing the specification (this can still be extremely useful). This can also be used to verify the correctness of various CS algorithms.
2. As a language that can be used to check an implementation for conformance against a formal specification to provide a high degree of assurance they match. Examples of this include Isabelle for the microkernel seL4 (a recent post on HN) and Coq for the CompCert certified C compiler (apparently used by Airbus in some capacity and some other safety-critical industries).
3. As a language that can be directly used to generate code (or is in fact compiled/interpreted directly) and prove interesting properties about said code. There's a light version of languages like this in the form of languages like SPARK or analyzers on top of SystemVerilog Assertions, but these bear only a passing resemblance to something like Arend. They are, however, in use by essentially every big chip manufacturer and are widely used again in safety-critical industries. There are languages closer to Arend that try to accomplish something similar, such as again Coq and Isabelle (which allow for extraction of a runnable program in addition to being provers), but I'm not aware of high-profile usages of those.
As far as I'm aware currently Arend is capable of doing the first. I'm not sure if it can do the second. I see no indication it can do the third. Crucially all this can be added later, potentially with little to no modification of the language.
The third use case means in theory these languages (Coq, Isabelle, Arend, etc.) could be used to write ordinary programs. In practice few people do because it's very time-consuming, the tooling is subpar, and there isn't much of a community doing this.
Arend is exciting to me because JetBrains could make a huge dent in the problems of tooling and community (see Kotlin). However, it's unlikely that even if JetBrains gave this its full support suddenly we'd have people writing ordinary web services with Arend. But it might just make other projects with high but not critical safety requirements (e.g. stuff like Kubernetes, Kafka, or at least small modules thereof) plausible to either verify or write directly with Arend.
Imagine if this were just a program you could run that returns 'true' or 'false'
As another poster said, it seems like they are trying to build their own version of Microsoft Research. It is also entirely feasible JetBrains wants to build out these concepts to further enhance their core products. Detecting and executing refactor opportunities across complex, strongly-typed codebases could have some synergy with this research and tooling.
A language like Agda does have good emacs support and can do useful things like help you fill in holes. But every speed bump on the way to setting up a theorem prover is important because the target audience isn’t necessarily programming experts who will go through a lot of pain so long as they can use emacs at the end of it.
1) Nice to see that the pipe is only a | and not |> like in Elixir. One character is better than two (and a Shift key.)
2) {- comment -} probably comes from another language (which one?) but I'm always surprised by the cleverness of language designers, even when there is no need for it.
3) The backslash before the keywords is a backslash, pun intended. Why is that necessary and why did somebody even think about it? Cleverness fails designers sometimes.
4) I like that this-is-a-valid-identifier. This_is_slower_to_type because of the shift keys. ThisIsNotMuchFaster.
Then I'm also wondering what the language is being used for now. Somebody else asked the same question and got downvoted but it looked like a honest question. Is it still borderline to research and will maybe influence mainstream languages or are we already unknowingly using some program written in Arend on our machines or somebody's else server?
Haskell has {- -} style (multiline)comments.
On an unrelated note, this-is-a-valid-identifier also in Lisp, but weirdly enough, the parens "( )" require shift. I think Lisp should use "[ ]" as parens because they do not require shift on modern keyboards.
I switch the layout of my non English keyboard in all coding windows and my fingers know what to press there.
> [define [plus i j] [+ i j]]
> [plus 1 2]
3What is the pun? Or, I guess I mean, what is the meaning of the second occurrence of 'backslash'?
Not so immediate, I admit.
But (IIUC) without coherence?