bor0

I like an environment that feels sane and logical and where I am not facing loads of incidental complexity along the way

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...

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.

It's a good post, but heavily OS dependant. For example, on my Mac:

  $ ls /dev/null /dev/full
  ls: /dev/full: No such file or directory
  /dev/null

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).

The whole article builds on the premise that the main point of every programming language is adoption and growth, while for Haskell we have

avoid success at all costs

According to that statement, to me it seems that the current "success" (however one defines it) of Haskell is just a side-effect.

Yes, it is used in industry, but I believe the bigger impact here is how other languages "steal" features from it.

Wow. PEiD, ResHacker, IDA. This brought memories. Same tools seem to be used as it was 15+ years ago.

No offence taken! Your first comment was constructive. I am looking forward to make the paper better.

Hi! Author here. First of all thanks to whoever shared this on HN, it was amazing to see it on the front page :)

but it's not really what it claims to be at all

I agree that the content may be interesting (only) to Coq newcomers, but I disagree with the quoted statement.

If you extract the code to Haskell e.g., and put some IO handling you basically have a line editor.

the length of the paper almost halves and the amount of substance becomes clearer

Thank you for this. I can amend it in a future version once I get more/other comments on the paper.

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 :)

https://bor0.wordpress.com

I blog about math and programming. It is a random collection but mostly (but not only) functional programming, formal verification.

TIL about most of this. Thanks for the detailed explanation.

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?

I usually write a book review post on my blog that contains these highlights. Whenever I need to recall something, I am reading my own posts.

I guess this is similar to spaced repetition.

I've written my first book entirely in Vim. Using Leanpub's support for Markdown+LaTeX was a very pleasant experience.

Exactly why I switched from Xubuntu to Mac 5 years ago. I just want to do my work, not fix my system after every minor upgrade.

Contributions to open source software. Knowing that the code I wrote runs on millions of machines feels great.

Also, another favourite project of mine is my book, written in Markdown+LaTeX and hosted with Git. Writing and editing experience was great.

The lack of syntax makes python a great language for prototyping

And I thought Lisp had a lack of syntax.

Get married and have kids. They are my biggest inspiration for all successes that I have.

This is an excellent answer! With the ever-changing frameworks and libraries, I couldn't agree more.

Rel: https://news.ycombinator.com/item?id=16352336

Hacking for sure is different nowadays, but that does not stop anyone from learning and understanding more.

Let's agree that re-inventing the wheel makes one more experienced, and also that it helps understanding things better. I believe that this distinction is what makes one a good/true programmer, compared to just lego play.

Edit: Also, I disagree that re-inventing the wheel is just busywork. Compare a programmer that just uses .sort() and another one that uses .sort() and implemented his own sort (disregarding the fact that he is not using his own sort) and really understands the math behind it. Which one would you rely on?

Programmers do not need to write much code anymore; all they need to do in most cases is wire together already available components.

As if this stops you from re-inventing the wheel in attempt to understand more. Understanding things is what distinguishes programmers.

I had exactly the same discussion with one of my friends that wants to become a programmer. His argument was that programming is not fun at all because all we do is use libraries and frameworks. My counter-argument was the paragraph above.

I also have a job, wife, kids, house, non-tech friends. However, at one point in my life I lived a very "closed" life, sitting in my room by myself and self-learning stuff (hacking Delphi/Pascal, then some Assembly x86, then C). It was definitely fun at the time.

Learning Idris will definitely alter the way you think about programming and make you a better programmer, even if you don't program in it on a daily basis.

To me, personally, the biggest barrier was lack of a proper introduction with a lot of examples.

I try to break this barrier a bit with my upcoming book: Gentle Introduction to Dependent Types with Idris.

I am very interested in this area but it is impossible for newcomers to get a grasp of it without too much digging. Logical Foundations was OK but I was still missing the theoretical explanation ("why does this tactic work? it is magic!").

So with accumulated knowledge from IRC, forums I hope to address this.

World of Warcraft with TeamSpeak/Ventrillo. However I have stopped playing it almost a decade ago.

Design patterns get obsolete. Programming languages get obsolete. Libraries get obsolete.

Mathematics doesn't. Learn CS foundations, logic, proofs to get better at understanding and gain abstraction experience.

Edit: books: How to prove it by D.Velleman, Proofs and concepts, Discrete Math by S.Epp

As the top voted answer says, proofs are at a very high level compared to programming.

Now imagine writing proofs on a very low level (check Metamath) where you work with wff and rewrite rules. It gets as tricky as programming.

Very good suggestion. Here's is a similar but free book: http://people.uleth.ca/~dave.morris/books/proofs+concepts.ht...

In around 2001 I started reverse-engineering games on the PC before having any programming skills (later moved to programming).

I remember MadWizard's assembly tutorial[0] being very helpful at the time.

[0] http://www.madwizard.org/programming/tutorials/