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.
2
6
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!