I have been very productive by the recent Spec-driven Agentic tools like Kiro, Spec-kit, and cc-sdd. The idea is to generate specified requirements before generating code.
I saw SpecLogician embracing Behaviour-Driven Development. Is there any tool for Type-driven development? See Thinking with Types.
SpecLogician flow is Gherking Spec → FormalSpec → IPL Machine. Type-driven programming flow is English Spec → Type declaration → Functional Code. The latter does not enjoy complete correctness but is more readable and allows quicker prototyping iteration. That’s why Python with typing and Typescript are popular sweetspots.
Discussion
Does Imandra have plans for supporting type-driven programming?
What do you think of generating IPL State Machines from type declarations as an optional step for some modules?
Hi, @mostafatouny – great question! We too are big fans of Kiro and Spec-kit and spec-driven development more generally. Yes, we do have plans for Type-Driven Development. For ImandraX, specs can be written as a combination of types and predicates (in the dependently typed world, all predicates get expressed as types; in ImandraX’s computational Higher-Order Logic, the type system is intentionally kept simple (Hindley-Milner based) and complex properties beyond the type system’s expressibility are written as executable predicates).
So, the equivalent of T(ype)DD in Imandra is ‘(executable Imandra spec)-driven development’ – but yes, this is a big part of what we are building and is in many ways available already with CodeLogician. We’re actually working on an integration with Kiro which we will share with you soon!
In the meantime, we’d love to hear your experience using ImandraX and CodeLogician if you can share.
I see Imandra has a great potential; Software engineering is shifting to those who will be able to write a well-specified documentation. Formal methods and type-driven dev were perceived as unnecessarily stages; nowadays, they are turning to be the quickest method to generate a maintainable code.
For sure I’ll share my experiences with the community here.