Incidentally, when you post articles like this, please don't use a title that makes it sound like an obituary.
Fortunately there is a lot of work in progress to improve the situation.
Did you mean they're not in wide use?
Where are the toolchains, IDEs, libs, etc for those?
I haven't used Idris, but as a proof assistant, Coq is one of the best computer games I know[1]. As a programming language, it's a very good proof assistant.[2]
[1] Really! It's fun. I've found the resulting proofs impossible to read, though. The closest description I can make is that they're programs for a stack machine; reading those is not a skill I've developed.
[2] All of the dependently typed languages, like Coq, that I've seen have not been very good programming languages, in my opinion. Except for ATS, which I don't think is a good programming language for different reasons. But I really like it, anyway.
Yeah, that's why I'm looking at Idris - it seems like the only one that's oriented towards practical programming. I did eventually get it installed, but it's tough going doing anything with it when you don't know Haskell tbh.
Whether you like ATS or not, it's very oriented towards practical programming. Also, ATS mostly looks bad IMO because of the style the author uses.
I still haven't fully formed an opinion on ATS though. Idris does seem really cool and stuff like enforcing time/space usage through the type system excites me.
ATS is based on ML (the author started with Dependent ML), but the code has a very imperative feel, leading to statements like "let () = expr() in ..." and "let x = ... in ()".
The stuff at http://www.ats-lang.org/Examples.html is just hideous, by the way.
----------------- Copying File ----------------
Authors version:
fun
fcopy (
inp: FILEref
, out: FILEref
) : void = let
val c = fileref_getc (inp)
in
if c >= 0 then let
val () = fileref_putc (out, c) in fcopy (inp, out)
end // end of [if]
end (* end of [fcopy] *)
My version:
fun fcopy (
inp: FILEref,
out: FILEref
) : void = let
val c = fileref_getc (inp)
in
if c >= 0 then let
val () = fileref_putc (out, c) in fcopy (inp, out)
end
end
fun
fib (
n: int
) : int =
if n >= 2 then fib (n-2) + fib (n-1) else n
fun fib ( n: int ) :
int = if n >= 2 then fib (n-2) + fib (n-1) else n
Authors Version:
fun
fibc (
n: int
) : int = let
fun loop (n: int, f0: int, f1: int) =
if n > 0 then loop (n-1, f1, f0+f1) else f0
// end of [loop]
in
loop (n, 0, 1)
end // end of [fibc]
fun fibc ( n: int ) : int =
let
fun loop (n: int, f0: int, f1: int) =
if n > 0 then loop (n-1, f1, f0+f1) else f0
in
loop (n, 0, 1)
end