Hacker News Reader

Generally, the computer will assist you in this endeavor

Kinda. Let's be honest: in production this often turns into a pain in the ass. There's some value in dependent typing, but providing evidence that concatenating UTF-8 strings is associative is not one of them.

View on HN

I have faith that this will get better. We need standard libraries of proofs just as much as we need standard libraries of code. I know Coq has made progress on this, but it's still early days.

I do agree with you that there are times when 'full' type checking is inappropriate. Typing is a spectrum, and it's a bit of an art to decide how detailed of guarantees to give for your API.

That is hilarious. And I also hope your joking.

That user is not joking, but note that you generally prove that string concatenation is associative once, not every time.

Reply on news.ycombinator.com