I’m super interested in this but it’s hard to follow. I really wish he spent more time elaborating, and editing. Took a few reads to even figure out why he would want to do this “and elimination”. I will be honest I’ve never proved anything in my life but I feel like this article would be near useless to anyone who has. So who is its target demographic, it seems too complicated for a beginner , but structured like its for people who know nothing.

It’s useful to someone who knows some formal logic but doesn’t know how that translates into programming. And elimination is a very basic operation when doing proofs. If you want to understand this I’d recommend reading a bit about formal logic first, try to understand formal logic on its own terms before looking at Curry-Howard. A quick google found me http://philosophy.hku.hk/think/pl/meta.php which looks vaguely reasonable.

Practically I’m not sure how many people will know formal logic without knowing anything about programming - philosophy majors maybe? - but also not everyone who knows about both will make the connection between them.

In University I had a Discrete Mathematics course that was very much proof and formal logic oriented.

Unfortunately, the class was taught in the Math department and not the Computer Science or Computer Engineering departments, so the class never really touched up on the intersection of formal logic and CS. I wish there was a follow-up course that would build on top of the purely math based one, but unfortunately that never happened.

On the one hand I do find it interesting, on the other the article is somewhat hard to read, and I genuinely found it slowing me down quite a bit. Words are used frequently but never defined or defined much later, such as “Connective”. For example, you define “holes” but we don’t figure out what that word means till much later. What does the “ | ” represent, seems like everything has one? In what way is the Unit “Useless”, and what does that mean? :( I’m sure you worked very hard to try and make this article accessible, but it’s still quite far from the layperson to be able to casually read it. It’s closer than most I’ve seen though, I think with some editing, more use of common English, and a bit of elaboration it could be MUCH simpler.

I’m super interested in this but it’s hard to follow. I really wish he spent more time elaborating, and editing. Took a few reads to even figure out why he would want to do this “and elimination”. I will be honest I’ve never proved anything in my life but I feel like this article would be near useless to anyone who has. So who is its target demographic, it seems too complicated for a beginner , but structured like its for people who know nothing.

It’s useful to someone who knows some formal logic but doesn’t know how that translates into programming. And elimination is a very basic operation when doing proofs. If you want to understand this I’d recommend reading a bit about formal logic first, try to understand formal logic on its own terms before looking at Curry-Howard. A quick google found me http://philosophy.hku.hk/think/pl/meta.php which looks vaguely reasonable.

Practically I’m not sure how many people will know formal logic without knowing anything about programming - philosophy majors maybe? - but also not everyone who knows about both will make the connection between them.

In University I had a Discrete Mathematics course that was very much proof and formal logic oriented.

Unfortunately, the class was taught in the Math department and not the Computer Science or Computer Engineering departments, so the class never really touched up on the intersection of formal logic and CS. I wish there was a follow-up course that would build on top of the purely math based one, but unfortunately that never happened.

Did you find the article useful then? Sounds like you’re exactly the target audience.

I see, I was coming from the opposite side :P. Makes sense.

I wrote a post on a similar(-ish) topic a while back. You may find it interesting.

https://tel.github.io/posts/types_of_data/

On the one hand I do find it interesting, on the other the article is somewhat hard to read, and I genuinely found it slowing me down quite a bit. Words are used frequently but never defined or defined much later, such as “Connective”. For example, you define “holes” but we don’t figure out what that word means till much later. What does the “ | ” represent, seems like everything has one? In what way is the Unit “Useless”, and what does that mean? :( I’m sure you worked very hard to try and make this article accessible, but it’s still quite far from the layperson to be able to casually read it. It’s closer than most I’ve seen though, I think with some editing, more use of common English, and a bit of elaboration it could be MUCH simpler.