Hey, author here! Thank you for recommending my book. I am always happy when someone else finds my work useful :)
> Anyone know if there's a decent way to get a printed copy?
I decided to re-publish the book with Apress, and it should be ready for print by March this year.
> How is it better than tdd in Idris book?
I would not say it is better, or worse. I read TDD and it's a great book, but it was mostly focused on practical stuff (i.e. programming in Idris), and I found it lacking the theoretical explanations (for example, what proofs are and how to do a mathematical proof, or what is a type-checker and how to implement one) which I hoped to cover in my book.
Adding onto the authors’s own review, I liked the second part on learning Idris but for my purposes the real gem was that it took me from zero prerequisites to a good intuition for dependent type theory in a very clear way that prepared me to go even deeper into topics like Homotopy Type Theory. The works I treasure are those that can build understandings of really complex topics without the crutch of a lot of prior assumed knowledge. It takes incredible clarity to do that well. This was one of my favorite book finds of recent years.
Computation has been and is a huge part of my life, and thanks to it I live a decent life with my family. It also helped with self-esteem and other similar things.
But love? Love taught me things I couldn't imagine (in a positive way).
Rust would certainly not have existed in it's current form without Haskell.
There are many such “progenitor languages” that focus primarily on theoretical elegance such as Smalltalk, Scheme, and Haskell that might not see huge adoption but do inspire a rather lasting influence on many languages that grew far larger than they.
My comment regarding "substance" was rather snarky, and I apologise for that.
I suppose the point I was really trying to make is that whilst this is certainly a nice demonstration of how to prove properties of data structures in Coq, actually specifying and verifying vim would be a monumentally larger task, and critically, most of the effort would be in entirely different areas.
I should have phrased this better though and my tone was way off, so I'm sorry if my first comment caused offence; anyone promoting formal methods to the SE community at large is doing a great thing!
I just wanted to express my appreciation of this reply. I originally wrote a simple ":)." but it's not really how it works here on HN :). Anyway, thanks for not being stubborn and pedantic, this is part what makes most of HN nice.
I am a 100% newcomer to the world of formal proofs and certainly dont know Coq. Because your topic was down to earth and the proof you provided were simple, I was able to understand these proofs.
As such your paper made me aware of how this community builds papers and proofs, and I can understand how this will grow insanely in complexity. Thank you!
This is exactly what I did with my first book. It is available for free on Leanpub, but I charge minimum for Kindle/print using Amazon KDP.
I just wanted to get my message across and learn something on the way. It also sells relatively well, but that is a side-effect of my initial intentions :)
> we wouldn't want to go full Haskell and avoid success at all costs
Can you elaborate on that statement? To me, it implies that going with Haskell avoids success, but I might be missing something. If that really is the implication, can you explain?
When you become too well known, or too widely used and too successful [...] suddenly you can’t change anything anymore.
The fact that Haskell has up to now been used for just university types has been ideal [...] Now, however, they're starting to complain if their libraries don’t work, which means that we’re beginning to get caught in the trap of being too successful.
What I’m really trying to say is that the fact Haskell hasn’t become a real mainstream programming language, used by millions of developers, has allowed us to become much more nimble, and from a research point of view, that’s great. We have lots of users so we get lots of experience from them. What you want is to have a lot of users but not too many from a research point of view – hence the avoid success at all costs.
Does anyone have the original slide where he used this line? It would be interesting to see what contextual clues were there at the time.
Later it turned out to be a syntactic pun: https://twitter.com/simonmar/status/246335257677271040. The official interpretation seems to be "Don't make success your top priority, because success may compromise things you care about more", whereas the hilarious version would be "Whatever you do, make sure you don't succeed."
Haskell connoisseurs can add info. That is literally all I know about it, or more, since I just Googled half of it. I do recall reading those interviews at the time, no doubt via HN.
To me it means that the Haskell project is strictly an academic experiment and seems to avoid mainstream success for itself at all costs. Not that projects using it can't achieve success, just that it'll never be popular and tries very hard not to be, though not really with that intent.
You should try my (esoteric) programming language (theorem prover), Budge-TP :)
You might find useful my recent write-up about https://bor0.wordpress.com/2023/02/05/writing-your-third-pro...