5 ms·

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...
  - ed_balls 7y ago
    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.
    - yole 7y ago
      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.
      - ed_balls 7y ago
        API is copyrightable (see Google vs Oracle) JetBrains plugins depend on this API, so Oracle can say they are in the violation and demand a fee.
nextos 7y ago
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.
- im_down_w_otp 7y ago
  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.
- mcguire 7y ago
  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.
namelosw 7y ago
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.
Mikeb85 7y ago
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.
jey 7y ago
They give an origin story on that page: > 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.

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...
- ed_balls 7y ago
  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.
  - yole 7y ago
    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.
    - ed_balls 7y ago
      API is copyrightable (see Google vs Oracle) JetBrains plugins depend on this API, so Oracle can say they are in the violation and demand a fee.

nextos 7y ago

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.

im_down_w_otp 7y ago
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.
mcguire 7y ago
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.

namelosw 7y ago

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.

Mikeb85 7y ago

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.

jey 7y ago

They give an origin story on that page: > 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.