News for hackers. Stuff that matters.

A comment on Idris: A Language for Type-Driven Development. Parent comment

Re:Idris: A Language for Type-Driven Development by ihm on Friday January 20, 2023 @11:45AM (#34455751)
The most famous ones off the top of my head: Coq, Agda, Lean, Idris, ATS. Here's a list: https://en.wikipedia.org/wiki/Category:Dependently_typed_lan...
[ Parent | on HN ]
Re:Idris: A Language for Type-Driven Development by peter_d_sherman on Friday January 20, 2023 @11:53AM (#34455916)
That (and pages like that) are what I was looking for!

Thanks, much appreciated!

[ Parent | on HN ]
Re:Idris: A Language for Type-Driven Development by still_grokking on Saturday January 21, 2023 @05:48AM (#34465479)
Scala is missing on that list (even it doesn't have "full dependent types" Match-Types are quite close).
[ Parent | on HN ]
Re:Idris: A Language for Type-Driven Development by eggy on Saturday January 21, 2023 @10:16AM (#34466942)
I tried ATS after finding Rust difficult. Zig is becoming my C replacement, and ATS is like a C++ replacement, although, I am using SPARK2014 now, but I am looking into ATS' contracts. There is no lack of PLs as a tool for whatever you may need to do nowadays. It's refreshing compared to 1970s to 1980s for me.
[ Parent | on HN ]