13 ms·

Arend: Theorem Prover Based on Homotopy Type Theory by JetBrains

309 points by adamnemecek 7y ago

nutjob2 7y ago
For those who want to understand what Homotopy Type Theory is, here is the "standard text" free to download or online: https://ncatlab.org/nlab/show/Homotopy+Type+Theory+--+Univalent+Foundations+of+Mathematics https://ncatlab.org/nlab/show/Homotopy+Type+Theory+--+Unival...
- Smaug123 7y ago
  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.
  - krapht 7y ago
    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).
    - JadeNB 7y ago
      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.
    - Footpost 7y ago
      They are not mutually exclusive: - 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.
- nudpiedo 7y ago
  Thanks for sharing. So it is basically a research programming language implementing some modern mathematical theories?
  - alimw 7y ago
    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.
quickthrower2 7y ago
deleted
- binarycrusader 7y ago
  Apache 2.0: https://github.com/JetBrains/arend-lib/blob/master/LICENSE https://github.com/JetBrains/arend-lib/blob/master/LICENSE
karoofish 7y ago
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?
- j88439h84 7y ago
  JetBrains is a company and they made a product called "Arend"
  - kccqzy 7y ago
    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.
    - manojlds 7y ago
      It's in JetBrains Incubator.
      - tunesmith 7y ago
        https://research.jetbrains.org/groups/group-for-dependent-types-and-hott https://research.jetbrains.org/groups/group-for-dependent-ty...
- manojlds 7y ago
  https://github.com/JetBrains/Arend https://github.com/JetBrains/Arend
kccqzy 7y ago
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.
- taeric 7y ago
  Slime is quite capable. Just a few curves to get involved.
  - dan-robertson 7y ago
    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.
  - pjmlp 7y ago
    Last time I bothered it still was catching up with the likes of Alegro and such.
bayesian_horse 7y ago
Again the question: Why is this useful? Is this just for programming language research? What kind of projects would you want to use this language for?
- ganzuul 7y ago
  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.
  - Labo333 7y ago
    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!
    - hwayne 7y ago
      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!
- meuk 7y ago
  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.
  - wpietri 7y ago
sriram_malhar 7y ago
A tutorial or a few example of proofs would be nice. How does the experience differ from using Coq?
bitL 7y ago
Kuklev @ Göttingen turned his research into a plugin? Great! Can we get one for VSCode as well please?
namelosw 7y ago
Wow. Finally a prover with serious IDE support. 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.
- est31 7y ago
  AI used to be about expert systems during the last AI hype before this one.
- mirekrusin 7y ago
  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.
- pure-awesome 7y ago
  I've found the VS Code plugin for Microsoft's Lean Theorem prover to be quite nice as far as IDE support goes. https://leanprover.github.io/about/ https://leanprover.github.io/about/ https://github.com/leanprover/vscode-lean https://github.com/leanprover/vscode-lean
  - bjz_ 7y ago
    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).
- davidgrenier 7y ago
  And here I was thinking I could finally use something from them.
- baron_harkonnen 7y ago
  > 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.
tom_mellior 7y ago
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-reference/definitions/functions#lemmas 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 7y ago
  https://github.com/Odomontois/Tincat https://github.com/Odomontois/Tincat Not exactly you asked for but the only one I know.
  - tom_mellior 7y ago
    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.
    - syrak 7y ago
      > 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.
pmontra 7y ago
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?
- chenglou 7y ago
  1) That's a pattern match. Nothing to do with pipe
- _jn 7y ago
  2): Haskell.
- CaptainBern 7y ago
  > 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. Haskell has {- -} style (multiline)comments.
- HerrMonnezza 7y ago
  3) Backslash before keywords looks inspired by TeX to me.
  - js8 7y ago
    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.
xvilka 7y ago
Too bad it is Java. What about using proper, native compiled language? Like Rust, or OCaml.
dwohnitmok 7y ago
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.
- yole 7y ago
  This is a research project. At this time there are no plans to invest into it on the same level as we're investing in Kotlin.
  - dwohnitmok 7y ago
    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?
    - yole 7y ago
      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.
deleted 7y ago
[deleted]
- deleted 7y ago
  [deleted]
jey 7y ago
Wow, JetBrains has a whole HoTT and Dependent Types Research Group: https://research.jetbrains.org/groups/group-for-dependent-types-and-hott https://research.jetbrains.org/groups/group-for-dependent-ty...
- cschmidt 7y ago
  Why would they be working on something like this? Is it useful for JetBrain's line of work? I mean it is cool, but it makes me curious as to why.
  - ed_balls 7y ago
    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.
    - ckosidows 7y ago
      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.
      - BonesJustice 7y ago
        Can you even imagine what an Oracle-built IDE would be like? Perish the thought. (shudder)
        roca 7y ago
        No need to wonder. Experience it for yourself. https://www.oracle.com/tools/technologies/netbeans-ide.html https://www.oracle.com/tools/technologies/netbeans-ide.html
        folkrav 7y ago
        Worse, Jdeveloper. https://www.oracle.com/database/technologies/developer-tools/jdeveloper.html https://www.oracle.com/database/technologies/developer-tools...
ocfnash 7y ago
Wow, I am delighted to see this! 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 https://coq.inria.fr/refman/language/cic.html#typing-rules rather than the syntax of the language used for building these terms.
- cjfd 7y ago
  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?
  - ocfnash 7y ago
    Well they claim it is a HoTT (thus presumably univalent) and furthermore has higher inductive types, neither of which exist in Coq's CIC. For example, they emphasise that function extensionality is a theorem here: https://arend-lang.github.io/about/arend-features 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.
- askthereception 7y ago
  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. [1] http://drops.dagstuhl.de/opus/volltexte/2018/8475/ http://drops.dagstuhl.de/opus/volltexte/2018/8475/
auggierose 7y ago
Chuckle. What an odd choice to use HTT for a JetBrains theorem prover.
UK-Al05 7y ago
These sorts of new functional languages coming out will be a boon for jetbrains. Imagine doing program synthsis in an ide?
bob1029 7y ago
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.
- manigandham 7y ago
  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.
dllthomas 7y ago
"Classes are just records with additional functionality, which makes them into a haskell-style type classes." But (IIUC) without coherence?
- Blaisorblade0 7y ago
  Good point, but never seen typeclass coherence with dependent types (in either Coq or the various versions of the Agda design). Not sure for Isabelle.
  - dllthomas 7y ago
    I'm not sure I can name another language with coherence, dependant types or not. To be fair, even GHC is half-hearted about it.

309 points by adamnemecek 7y ago

For those who want to understand what Homotopy Type Theory is, here is the "standard text" free to download or online: https://ncatlab.org/nlab/show/Homotopy+Type+Theory+--+Univalent+Foundations+of+Mathematics https://ncatlab.org/nlab/show/Homotopy+Type+Theory+--+Unival...

Smaug123 7y ago
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.
- krapht 7y ago
  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).
  - JadeNB 7y ago
    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.
  - Footpost 7y ago
    They are not mutually exclusive: - 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.
nudpiedo 7y ago
Thanks for sharing. So it is basically a research programming language implementing some modern mathematical theories?
- alimw 7y ago
  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.

quickthrower2 7y ago

deleted

binarycrusader 7y ago
Apache 2.0: https://github.com/JetBrains/arend-lib/blob/master/LICENSE https://github.com/JetBrains/arend-lib/blob/master/LICENSE

karoofish 7y ago

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?

j88439h84 7y ago
JetBrains is a company and they made a product called "Arend"
- kccqzy 7y ago
  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.
  - manojlds 7y ago
    It's in JetBrains Incubator.
    - tunesmith 7y ago
      https://research.jetbrains.org/groups/group-for-dependent-types-and-hott https://research.jetbrains.org/groups/group-for-dependent-ty...
manojlds 7y ago
https://github.com/JetBrains/Arend https://github.com/JetBrains/Arend

kccqzy 7y ago

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.

taeric 7y ago
Slime is quite capable. Just a few curves to get involved.
- dan-robertson 7y ago
  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.
- pjmlp 7y ago
  Last time I bothered it still was catching up with the likes of Alegro and such.

bayesian_horse 7y ago

Again the question: Why is this useful? Is this just for programming language research? What kind of projects would you want to use this language for?

ganzuul 7y ago
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.
- Labo333 7y ago
  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!
  - hwayne 7y ago
    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!
meuk 7y ago
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.
- wpietri 7y ago

sriram_malhar 7y ago

A tutorial or a few example of proofs would be nice. How does the experience differ from using Coq?

bitL 7y ago

Kuklev @ Göttingen turned his research into a plugin? Great! Can we get one for VSCode as well please?

namelosw 7y ago

Wow. Finally a prover with serious IDE support. 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.

est31 7y ago
AI used to be about expert systems during the last AI hype before this one.
mirekrusin 7y ago
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.
pure-awesome 7y ago
I've found the VS Code plugin for Microsoft's Lean Theorem prover to be quite nice as far as IDE support goes. https://leanprover.github.io/about/ https://leanprover.github.io/about/ https://github.com/leanprover/vscode-lean https://github.com/leanprover/vscode-lean
- bjz_ 7y ago
  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).
davidgrenier 7y ago
And here I was thinking I could finally use something from them.
baron_harkonnen 7y ago
> 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.

tom_mellior 7y ago

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-reference/definitions/functions#lemmas 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 7y ago
https://github.com/Odomontois/Tincat https://github.com/Odomontois/Tincat Not exactly you asked for but the only one I know.
- tom_mellior 7y ago
  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.
  - syrak 7y ago
    > 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.

pmontra 7y ago

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?

chenglou 7y ago
1) That's a pattern match. Nothing to do with pipe
_jn 7y ago
2): Haskell.
CaptainBern 7y ago
> 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. Haskell has {- -} style (multiline)comments.
HerrMonnezza 7y ago
3) Backslash before keywords looks inspired by TeX to me.
- js8 7y ago
  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.

xvilka 7y ago

Too bad it is Java. What about using proper, native compiled language? Like Rust, or OCaml.

dwohnitmok 7y ago

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.

yole 7y ago
This is a research project. At this time there are no plans to invest into it on the same level as we're investing in Kotlin.
- dwohnitmok 7y ago
  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?
  - yole 7y ago
    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.

deleted 7y ago

[deleted]

deleted 7y ago
[deleted]

jey 7y ago

Wow, JetBrains has a whole HoTT and Dependent Types Research Group: https://research.jetbrains.org/groups/group-for-dependent-types-and-hott https://research.jetbrains.org/groups/group-for-dependent-ty...

cschmidt 7y ago
Why would they be working on something like this? Is it useful for JetBrain's line of work? I mean it is cool, but it makes me curious as to why.
- ed_balls 7y ago
  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.
  - ckosidows 7y ago
    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.
    - BonesJustice 7y ago
      Can you even imagine what an Oracle-built IDE would be like? Perish the thought. (shudder)
      - roca 7y ago
        No need to wonder. Experience it for yourself. https://www.oracle.com/tools/technologies/netbeans-ide.html https://www.oracle.com/tools/technologies/netbeans-ide.html
        folkrav 7y ago
        Worse, Jdeveloper. https://www.oracle.com/database/technologies/developer-tools/jdeveloper.html https://www.oracle.com/database/technologies/developer-tools...

ocfnash 7y ago

Wow, I am delighted to see this! 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 https://coq.inria.fr/refman/language/cic.html#typing-rules rather than the syntax of the language used for building these terms.

cjfd 7y ago
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?
- ocfnash 7y ago
  Well they claim it is a HoTT (thus presumably univalent) and furthermore has higher inductive types, neither of which exist in Coq's CIC. For example, they emphasise that function extensionality is a theorem here: https://arend-lang.github.io/about/arend-features 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.
askthereception 7y ago
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. [1] http://drops.dagstuhl.de/opus/volltexte/2018/8475/ http://drops.dagstuhl.de/opus/volltexte/2018/8475/

auggierose 7y ago

Chuckle. What an odd choice to use HTT for a JetBrains theorem prover.

UK-Al05 7y ago

These sorts of new functional languages coming out will be a boon for jetbrains. Imagine doing program synthsis in an ide?

bob1029 7y ago

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.

manigandham 7y ago
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.

dllthomas 7y ago

"Classes are just records with additional functionality, which makes them into a haskell-style type classes." But (IIUC) without coherence?

Blaisorblade0 7y ago
Good point, but never seen typeclass coherence with dependent types (in either Coq or the various versions of the Agda design). Not sure for Isabelle.
- dllthomas 7y ago
  I'm not sure I can name another language with coherence, dependant types or not. To be fair, even GHC is half-hearted about it.