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
[ Parent
| on HN ]
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).