Hello, Let’s say I want to do system/backend programming using a language with dependent types (just to give it a try). Which one of those would be the best considering agility of the programmer (I want to do software prototyping) and performance of the final executable (I want the final program…

After having read about them, I don’t think I would need linear types (I don’t really do system programming).

I might not need an FFI and be happy with pure functional programming. I’ll have to read from and write to disk at some point though. :wink:

Is the size of the user base of those languages known? I would guess Coq has a lot of users. Maybe the size of the user community is a good heuristic for the production-ready state of a language.

[image] UnixJunkie: I would guess Coq has a lot of users. I think these are mostly users who use if for proofs, not for “general” programming. But there are multiple books on “general” programming with Idris, so I think I would check out Idris or ATS first.

Hmm I would not be too optimistic about that, unless the properties carried by your molecules are rather simple and the proof that your function preserves these properties can be discharged automatically by the system that you use. My typical interaction with these systems is that your program will …

This book looks quite cool: " Type-Driven Development with Idris" [image] Type-Driven Development with Idris This book will turn your approach to software upside-down, in the best way.

This book is about certified programming. Which makes me think about writing programs hand in hand with a mathematical proof. That’s not what I want to do (I know the programmer productivity of such approaches is not for prototyping, it is for certification of software). I just want to write prog…

(Note : I’m not an active user of any of the systems, only spent some free time learning one of them, so salt etc) Programming with dependent types is same as writing proofs (by Curry-Howard correspondence), as brought up by @igarnier [image] igarnier: My typical interaction with these systems…

[image] UnixJunkie: This book is about certified programming. Which makes me think about writing programs hand in hand with a mathematical proof. That’s not what I want to do That is what programming with dependent types is for. If you don’t want that, then you don’t want to be working in a…

Has anyone mentioned Haskell yet? It has some support for dependent types AFAIK. In particular, take a look at liquid Haskell: https://ucsd-progsys.github.io/liquidhaskell-blog/

Which language to use for general programming with dependent types?

Learning

UnixJunkie August 29, 2018, 8:42am 9

This book looks quite cool: " Type-Driven Development with Idris"

Topic		Replies	Views
Dependent Types in the Purest Form Community announce	21	4976	October 15, 2022
How to become 10x OCaml developer? Learning	27	3931	July 25, 2019
Do you enjoy programming? Community	14	912	March 20, 2025
Is there any OCaml(not ML or StandardML) - inspired languages with dependent types and algebraic affects? Learning language , types	5	2327	November 20, 2017
Can OCaml "abstract above the code level"? Community	30	1134	February 17, 2024

Which language to use for general programming with dependent types?

Related topics