Conversation

Cliff

@field_strength

·

Aug 8, 2019

I'm pumped to try out this homotopy type theory language/IDE. About time we're able to code in a language whose core idea is from this millennium!

Quote Tweet

Brendan Zabarauskas

@brendanzab

· Aug 7, 2019

This looks pretty interesting! @ArendLang is a theorem prover based on homotopy type theory, with IDE support for IntelliJ: https://arend-lang.github.io

Show this thread

1

4

Brendan Zabarauskas

@brendanzab

Replying to

@field_strength

Sadly I don’t think tactics are implemented yet, so it might be a tad limited. Still seems worth a look though! Also would recommend checking out Cubical Agda 🙂

2:13 AM · Aug 9, 2019·Twitter for iPhone

Cliff

@field_strength

·

Aug 9, 2019

Replying to

@brendanzab

Yeah I saw the tutorial was pretty limited too and I seemed to hit the limit pretty quickly. Excited to see where this goes though! Hard to beat a type-checker as a source of intuition.