I think formal methods may take off sometime in the future, hopefully not too distant from now. But this has been a thing since the mid 90s, and tools might still not be mature enough.
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.
The reason I'm so excited about this development is that it's a commercial product-focused company putting a level of effort into polish and refinement into this domain. The lack of that kind of polish is an enormous inhibitor to adoption and acceptance of these classes of tools.
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.
For a look at the state of non-dependently typed formal methods, take a look at Frama-C and Ada Spark. Frama-C is pretty rough around the edges (and both have some significant limitations) but is amazingly useful while Spark is more constrained but has much better tooling.
A language (like Dafny?) with garbage collection plus the techniques behind those two would make for a very powerful toolset.
> 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.
I guess they might intrigued that dependent type would be the future of programming languages with rich IDE support.
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.
Most of their money come from providing tools for java world. If Oracle would decide to go into this market, they are screwed, hence Kotlin and other experiments.
What tools could Oracle feasibly replace? I'm aware of their broader product line, but I mostly use IntelliJ. I can't see Oracle replacing IntelliJ anytime soon.
Going into the market doesn't necessary mean building a replacement. I could also mean copyright and licensing. Sponsoring a plugin for Open Source editors. You gotta hedge your bets.
What exactly do you mean by "copyright and licensing"? JetBrains products do not violate any copyright or licenses from Oracle, and even if they change the license of future versions of Java, current versions are available for us to use. And Oracle has been investing into two different IDEs, NetBeans and JDeveloper.
Of course it is. Formal provers are great for analyzing code. For example, Nim has a formal prover for analyzing potential concurrency conflicts. Would definitely help in an IDE.
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.
Perhaps have a look at the paper "Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom" by Cohen et al. [1] which gives the typing rules in the early sections.
Yes, I came here to say precisely that. It looks like it has about the same things available as coq as far as syntax is concerned, so what are the differences?
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.
> It just doesn't attract eyeballs like machine learning and blockchains.
... 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.
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.... :)
Yeah, I've be _really_ impressed with Lean's support. Wish other provers like Coq and Agda were at the same level (I know how challenging it is to do though).
Proving systems are one of main areas of research in blockchain space; on different levels - at type level for contracts/vm, at consensus level regarding properties like liveness etc and at multiple cryptography levels ie. in area of zero knowledge computations.
I can't tell if this is JetBrains trying to develop its own version of Microsoft Research, or if this is the humble beginnings of a project like Kotlin that it aims to put its weight behind. Both would be cool (and indeed it could be both), but the latter would be truly exciting and a potentially a huge leap forward for theorem proving and formal verification.
Ah I figured it probably wouldn't be the same degree of commitment as Kotlin given the disparity of demand. Are you at liberty to say whether this is a project JetBrains hopes to eventually use in a production capacity for its own work?
I'm not in contact with the research team and don't know which practical applications they have in mind, but as far as IntelliJ is concerned, we don't have any current plans to use the results of their work.
Though note that it is not simple to understand; it will take quite a lot of real work to grok, unless for some reason you already know about univalence.
The trouble with HoTT is that it has very little to offer in regards to making it easier to prove the correctness of programs expressed in Hoare logic (which is ~99% of all computer programs).
- 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.
But the trouble with focusing effort on tools that can serve our current programs is that it guarantees that we are locked into our current programming models instead of exploring new design spaces.
While Homotopy Theory is just one strand in modern mathematics, it is believed that a type theory based on it can serve as a foundation for the whole of mathematics.
I found the language reference and see how to define types and expressions, but I can't find any examples of what proofs would look like. Has anyone dug in enough to link to an actual proof of something?
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.
Thanks. The only lemma in that repo is the following (in Cat.ard):
\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)
}
)
I'm not 100% sure what's going on but it looks like this would be a one-liner in Coq, something like (hand-waving here):
destruct C; auto using assoc, inv_inv.
So... yeah. Not enough data to come to a final conclusion, but I do wonder why people keep building more systems of this kind.
This repo was my first learning project.
I barely knew Idris, and have no experience with HoTT.
Please don't judge the language referring to this.
You can refer nice code here https://github.com/JetBrains/arend-lib
> I do wonder why people keep building more systems of this kind.
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.
True, there are probably no theoretical obstacles. But there is a huge implementation effort, and judging from other new proof assistants that started out without tactics, I wouldn't hold my breath.
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.
> Coq with tactics does not fair particularly well on anything more than toy examples
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?
Take a look at how much trouble the author had finding a working ST, despite there being widely published and used libraries at some point but which no longer work in newer versions of Coq. The author ended up using a very specific git hash version of the Iris library, and he admits the documentation of Iris is pretty much non-existent.
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.
* shrug* Coq users have the choice between using tactics and writing proof terms like Agda users. 99.9% of Coq users choose tactics 99.9% of the time. They might know something you don't know, or you might know something they don't know. You decide.
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.
Having used both, Coq proof terms aren't Agda proof terms. Coq provides neither "real" dependent pattern matching nor edit-time tactics. Long-term, the vision in Agda would be to support metaprogramming closer to what you do in FP languages. But even now, there are domains where Agda is competitive (tho they seem to be in mechanizing mathematical theories, as in, things designed by mathematicians to be compact). To prove software correct, you'll likely end up with with proofs you'll want to automate.
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'm very familiar with Adam's work. Now consider that he did a lot of work on Ynot, and as per this paper, Ynot no longer works with latest Coq.
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.
The "only" lemma is because other lemmas are defined via \func
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
The premise of an axiomatized system is that you can "mechanically" check proofs. So you can also invert the question and ask "Why the hell do we still prove things by hand?".
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.
I gather you understand the topic, but I'm still left wondering: who is this for, and what will they do with it?
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?
> I gather you understand the topic, but I'm still left wondering: who is this for, and what will they do with it?
'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
It's a mighty interesting topic, and unfortunately, I've also found it quite difficult to get more than a shallow understanding of it.
A shot in the dark: it could perhaps help in automatically optimizing algorithms by proving that the optimized version is equal to an easily written and reasoned about.
I think reasoning about correctness is easier than about optimizations. Even if you account for a simple complexity model (real computers are a lot more complex, because of techniques like branch prediction or memory caching), proving an implementation as optimal is very hard!
It's often really hard to know if an optimization is "correct"- is the same function as the original, unoptimized version. Formal methods helps here by showing they're equivalent, so you can focus on finding good optimizations instead!
I sympathize with you but I always follow develooments in this space because the potential upside is so awesome. Excellent mathematicians are using theorem provers to check their logic, and such a system brought to say the compilation of a realtime OS, or a distributed transactional system could provide a real safety net for preventing logical errors introduced by new code.
I do get that point, but it seems to me that only very advanced programmers are able to work with such languages and systems.
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.
For most of the cases where formally verifying _code_ is important, "unit tests" aren't enough. If the person who writes the proofs leaves, you hire someone else to write proofs. Otherwise you don't have a business model.
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.
"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. " - That's because we're an immature field. Something like this will eventually have to come out in order to fix the crisis in software.
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 do get that point, but it seems to me that only very advanced programmers are able to work with such languages and systems.
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.
"who's going to maintain this shit when that rock-star theorem guy is gone?"
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.
I am dont know so much about that field but I "feel" the same. It would be nice if someone who knows that stuff could reply here if this intuition is right or not. Eventually when we reason about our code "as standard" non-math programmers we are doing math & logic & proofs in our minds aren't we? And we capture the edge cases in forms of tests and hope for the best if we thought about and enumerated all the necessary ones.
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.
Well, look who’s afraid for their job to be taken by someone else.
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.
In short to give a confidence in correctness of a program that often exceeds that of other techniques (such as testing). More specifically, from the viewpoint of a programmer there's three general ways that a language like this is useful. I'll use examples from this general class of languages (theorem provers) since Arend is still in its infant stages.
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.
JetBrains has been gaining a lot of stock with me lately. I recently discovered that Rider is an extremely compelling replacement for VS2019 (for C# codebases), and this kind of news is going to keep them on my radar for the foreseeable future.
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.
Rider is basically taking Resharper (their VS extension that has been around for years) and merging it into their own IntelliJ IDE platform. It removes the performance and integration limitations and is fantastic to use.
This is extremely exciting as very few functional languages have good IDE support. I'm quite excited to see how building in IDE-support from the get go would help things.
The IDE features of slime are quite different to the ones one would want in a theorem prover. In particular many functional languages that aren’t CL have strong type systems (so you’ll want feedback about the types of things) and poor introspection (so something like swank isn’t so easy).
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.
Knowing nothing about Homotopy Type Theory and looking at the language only for the way it looks:
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?
1) those are for pattern matching, or sum-type separators in data definitions. Also if `|` were to mean "pipe", it's actually a downgrade because the direction isn't clear. `|>` and `<|` show that they pass data to the right and left functions respectively. If it were `|` what would be the accompanying operator that passes data in the opposite direction? Unix pipe streams data, but these operators are actually function application, so I wouldn't conflate the two, the latter is a much simpler concept, `a |> f == f(a)` and `f <| a == f(a)`.
> 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.
I actually kinda like the idea. The concept of (limited set of) "reserved keywords" always annoyed the mathematical purist in me.
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.
You mean, modern English keyboard layouts! Square brackets require alt(gr) on my keyboard. Seriously, most European layouts are ridiculously coding-unfriendly.
"this-is-a-valid-identifier" isn't because you don't know if this is an algebraic expression or not. Not sure how this language disambiguates, if it's using spaces or some other symbol.
All "cleverness" usually comes from struggle with parser generator. It's too many languages in the wild with weird syntax due to lack of interest/skills in proper parser.
i'm a little confused. Is this BY Jetbrains as the title says, or by another company? Its using the same style as the Jetbrains website and and says "By" but also says Arend?
Is this actually an official product by JetBrains though? The github repo shows majority of commits by a single person. This looks more like a 20% time project by an engineer at JetBrains.
