News for hackers. Stuff that matters.
Re:Show HN: Dependently typed language for proofs that you c... by jimsimmons on Saturday October 02, 2021 @02:47AM (#28726541)
Cool! No offence, I went on a rant hoping to start a discussion about FP. The fact that you have a dependently typed language in 1000 lines is an amazing feat. Don’t want to take anything away from that. I just wish the functional community took readability more seriously is all
Re:Show HN: Dependently typed language for proofs that you c... by tluyben2 on Saturday October 02, 2021 @03:04AM (#28726613)
Maybe it is because of when you are doing this all day, you really don't see this anymore? I can read j/k just fine, as well as Haskell, but I find many imperative languages noisy and basically ugly and unreadable. I like things terse and as much as I can on 1 screen so I don't have to scroll or remember things (when you get older, remembering wtf something was called again gets pretty annoying; very strict static typing and defining types precisely (aka a zipcode or telephone number are not strings!) together with terse functional constructs help a lot; the IDE will know everything so you can focus on implementation).