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.
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.
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.
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.
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.
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.
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.
"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?
[+] [-] jey|6 years ago|reply
[+] [-] ocfnash|6 years ago|reply
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.
[+] [-] askthereception|6 years ago|reply
[1] http://drops.dagstuhl.de/opus/volltexte/2018/8475/
[+] [-] cjfd|6 years ago|reply
[+] [-] namelosw|6 years ago|reply
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.
[+] [-] baron_harkonnen|6 years ago|reply
... 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.
[+] [-] pure-awesome|6 years ago|reply
https://leanprover.github.io/about/ https://github.com/leanprover/vscode-lean
[+] [-] mirekrusin|6 years ago|reply
[+] [-] est31|6 years ago|reply
[+] [-] davidgrenier|6 years ago|reply
[+] [-] dwohnitmok|6 years ago|reply
[+] [-] yole|6 years ago|reply
[+] [-] nutjob2|6 years ago|reply
https://ncatlab.org/nlab/show/Homotopy+Type+Theory+--+Unival...
[+] [-] tom_mellior|6 years ago|reply
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.
[+] [-] optician_owl|6 years ago|reply
[+] [-] sriram_malhar|6 years ago|reply
[+] [-] bayesian_horse|6 years ago|reply
Is this just for programming language research? What kind of projects would you want to use this language for?
[+] [-] meuk|6 years ago|reply
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.
[+] [-] ganzuul|6 years ago|reply
[+] [-] bitL|6 years ago|reply
[+] [-] bob1029|6 years ago|reply
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.
[+] [-] manigandham|6 years ago|reply
[+] [-] kccqzy|6 years ago|reply
[+] [-] UK-Al05|6 years ago|reply
[+] [-] pmontra|6 years ago|reply
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?
[+] [-] Shoue|6 years ago|reply
[+] [-] CaptainBern|6 years ago|reply
Haskell has {- -} style (multiline)comments.
[+] [-] HerrMonnezza|6 years ago|reply
[+] [-] chenglou|6 years ago|reply
[+] [-] raverbashing|6 years ago|reply
[+] [-] bvrmn|6 years ago|reply
[+] [-] JadeNB|6 years ago|reply
What is the pun? Or, I guess I mean, what is the meaning of the second occurrence of 'backslash'?
[+] [-] unknown|6 years ago|reply
[deleted]
[+] [-] _jn|6 years ago|reply
[+] [-] dllthomas|6 years ago|reply
But (IIUC) without coherence?
[+] [-] Blaisorblade0|6 years ago|reply
[+] [-] karoofish|6 years ago|reply
[+] [-] j88439h84|6 years ago|reply
[+] [-] manojlds|6 years ago|reply
[+] [-] auggierose|6 years ago|reply
[+] [-] quickthrower2|6 years ago|reply
[+] [-] binarycrusader|6 years ago|reply
[+] [-] unknown|6 years ago|reply
[deleted]
[+] [-] unknown|6 years ago|reply
[deleted]
[+] [-] xvilka|6 years ago|reply