2 ms·
The fact that he mentions type driven development probably means that he has dependent typing around, probably as seen in the language Idris, whose recently pub
by tines 10y ago
The fact that he mentions type driven development probably means that he has dependent typing around, probably as seen in the language Idris, whose recently published book is called the same. Idris is very much not just an abstract language.
- devrandomguy 10y agoYes, the author mentioned Idris shortly afterwards, but I get the impression that this is just the tip of an iceberg. Idris was presented as the one example that is most likely to evolve from a research-only language, to a production language.
- dllthomas 10y agoThere's also agda and coq, at various points on the spectrum between programming language and theorem prover.