This looks pretty interesting! is a theorem prover based on homotopy type theory, with IDE support for IntelliJ:
Conversation
There's an announcement post here for those interested: groups.google.com/forum/#!topic/ - gives a bit more background into why is working on it!
2
1
Seems like it's mainly there to explore how modern IDEs could be used for theorem proving, which I think is a great goal! Would be cool to see more creators of dependently typed programming languages looking beyond Emacs, to supporting things like the Language Server Protocol.
Oh wow, it seems they have a whole research group working on it: research.jetbrains.org/groups/group-f
1
1
Agreed! I'll definitely be checking Arend out. The best IDE experience for dependent types I've seen so far is Lean in VSCode
1
1
Agreed! Really would like to see Agda and Coq follow in that regard!
1
This Tweet was deleted by the Tweet author. Learn more
Yeah, it’s one of the reasons I get more use out of Lean than Agda or Coq.