Programming

22258 readers

963 users here now

Welcome to the main community in programming.dev! Feel free to post anything relating to programming here!

Cross posting is strongly encouraged in the instance. If you feel your post or another person's post makes sense in another community cross post into it.

Hope you enjoy the instance!

Rules

Follow the programming.dev instance rules
Keep content related to programming in some way
If you're posting long videos try to add in some form of tldr for those who don't want to watch videos

Wormhole

Follow the wormhole through a path of communities !webdev@programming.dev

founded 2 years ago

MODERATORS

snowe@programming.dev

Ategon@programming.dev

MaungaHikoi@lemmy.nz

UlrikHD@programming.dev

Beyond Booleans - “bool expressions” in Lean, proposition, proof (overreacted.io)

submitted 3 days ago by Kissaki@programming.dev to c/programming@programming.dev

1 comments fedilink hide all child comments

Explores how the Lean programming language handles 2 + 2 = 4, which other programming languages collapse into a bool, but Lean considers a Proposition, and requires Proof.

How does provably correct programming look? This article seems to give a good introduction and example.

top 1 comments

sorted by: hot top controversial new old

[–] FizzyOrange@programming.dev 8 points 3 days ago

This is an unbelievably good explanation of some very difficult concepts. I think the Lean documentation should start with an enormous link to this post.

Highly recommended to anyone interested in Lean who isn't already an expert.