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.
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.
> 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.
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.
https://www.oracle.com/database/technologies/developer-tools...