General Dev>In The News

"Why not just use Lean?"

CommunityNews

CommunityNews

"Why not just use Lean?"

I have been told that when proposing to formalise mathematics these days, you have to explain why you are not using Lean. And that reminds me why I left the dependent-typed world 40 years ago: its cultism, insularity and conformity. Lean is a great language with good tools, a large library and a huge, enthusiastic user community that has lately accomplished astounding things. But let’s not forget that the formalisation of mathematics goes back nearly 60 years. Amidst the hype around today’s progress, we must remember how we got here. It was not by people following the crowd.

Read in full here:

View thread on forum
#lean
0 1 0

Where Next?

View thread on forum
lean
Home General Dev>In The News
#lean
0 1 0
Last post

Popular General Dev topics Top

First poster: bot
General Dev>In The News

20 patterns to watch for in your engineering team (pdf)
A field guide to help you recognize achievement, spot A field guide to help you recognize achievement, spot bottlenecks, and debug your d...
pluralsight.com
0 1347 0
New
First poster: bot
General Dev>In The News

Developing Godot Projects with Neovim
Developing Godot Projects with Neovim. When I started using Godot Engine, what surprised me the most is the built-in Language Server Pro...
devpoga.org
/neovim
0 1983 0
New
First poster: bot
General Dev>In The News

A more mature ChatGPT competitor? PaLM + RLHF - Pytorch (wip)
GitHub - lucidrains/PaLM-rlhf-pytorch: Implementation of RLHF (Reinforcement Learning with Human Feedback) on top of the PaLM architectur...
github.com
#chatgpt
0 1415 0
New
First poster: bot
General Dev>In The News

Introducing the ChatGPT/LLM error tracker
Large Language Models like ChatGPT say The Darnedest Things. The Errors They MakeWhy We Need to Document Them, and What We Have Decided ...
garymarcus.substack.com
#error#chatgpt
0 3521 0
New
First poster: bot
General Dev>In The News

A reason why Mac speakers sound better and louder than most
Hector Martin (@marcan@treehouse.systems). Attached: 1 image For those wondering why the hell we need all this safety system stuff for...
social.treehouse.systems
0 1576 0
New
First poster: bot
General Dev>In The News

Declarative GNOME configuration with NixOS
Declarative GNOME configuration with NixOS. I adore tinkering with my machine, trying new tools, extensions, themes, and ideas. When I w...
hoverbear.org
/nixos
0 1557 0
New
CommunityNews
General Dev>In The News

Perplexica: Open-Source Perplexity Alternative
GitHub - ItzCrazyKns/Perplexica: Perplexica is an AI-powered search engine. It is an Open source alternative to Perplexity AI. Perplexic...
github.com
0 1794 0
New
First poster: jkdiaz
General Dev>In The News

Dark mode is not as good for your eyes as you believe (2019)
Dark mode isn’t as good for your eyes as you believe. The shadowy display mode has leagues of fans claiming it helps reduce eye strain, ...
wired.com
3 1587 2
New
CommunityNews
General Dev>In The News

SLUM: The Shadow Library Uptime Monitor
SLUM: The Shadow Library Uptime Monitor. This dashboard tracks the availability of popular shadow libraries in real time from a US-based...
open-slum.org
#library#monitor
0 2891 0
New
CommunityNews
General Dev>In The News

The Meter, Golden Ratio, Pyramids, and Cubits, Oh My
The French originated the meter in the 1790s as one/ten-millionth of the distance from the equator to the north pole along a meridian thr...
iforgeiron.com
0 592 0
New

Other popular topics Top

PragmaticBookshelf
Backend>Learning Resources

Testing Elixir
Write Elixir tests that you can be proud of. Dive into Elixir’s test philosophy and gain mastery over the terminology and concepts that u...
pragprog.com
#pragprog/elixir#published-book/book-testing-elixir
33 5004 8
New
DevotionGeo
Backend>Chat

What is the reason behind Rust’s web framework, Rocket, not performing as well as expected in the Techempower benchmarks?
I know that these benchmarks might not be the exact picture of real-world scenario, but still I expect a Rust web framework performing a ...
#web-frameworks/rust
36 7463 11
New
AstonJ
General Dev>Hardware

BIIP MT3 Extended 2048 Custom Keycap Set (Drop)
This looks like a stunning keycap set :orange_heart: A LEGENDARY KEYBOARD LIVES ON When you bought an Apple Macintosh computer in the e...
/keyboards#apple#keycaps#mechanical-keyboards
14 6713 7
New
Exadra37
Linux>Questions

What is the most minimalist Linux server distro?
I am asking for any distro that only has the bare-bones to be able to get a shell in the server and then just install the packages as we ...
#linux#servers
66 25846 24
New
AstonJ
General Dev>Dev Chat

Languages Without Garbage Collection
Continuing the discussion from Thinking about learning Crystal, let’s discuss - I was wondering which languages don’t GC - maybe we can c...
#garbage-collection
21 5575 7
New
First poster: CommunityNews
AI>In The News

How to fix the eyes in AI-generated images
aidemos.info
0 4508 0
New
DevotionGeo
General Dev>Questions

Do you prefer regular mechanical keyboards or low profile mechanical keyboards and why?
I have always used antique keyboards like Cherry MX 1800 or Cherry MX 8100 and almost always have modified the switches in some way, like...
/keyboards#mechanical-keyboards
27 5496 10
New
PragmaticBookshelf
General Dev>Learning Resources

Write Better with Vale
Lint your docs like code: turn any style guide into enforceable rules with Vale and publish clear, consistent content every time. ...
pragprog.com
#pragprog#published-book#vale/book-write-better-with-vale
8 9973 5
New
PragmaticBookshelf
Backend>Learning Resources

Programming Clojure, Fourth Edition
Quickly turn complex problems into simple, working solutions using functional programming, safe concurrency, and the expressive tools of ...
pragprog.com
#pragprog
4 1975 3
New
xiji2646-netizen
AI>Chat

Has anyone tried the Karpathy CLAUDE.md rules? (97.8k stars)
There’s a GitHub repo at forrestchang/andrej-karpathy-skills that’s sitting at 97.8k stars. It’s a single CLAUDE.md file with four behavi...
#claude
0 37 1
New
Back to top

Sponsor Spotlight

WyewWorks

Enabling companies to succeed by building software people love.

General Dev>In The News

General Dev In The News ❯

Latest on Devtalk

Devtalk ❯

We ❤️ helpful members!

We reward our most helpful members via our MOTM scheme - by giving away a whopping 25 books per year!

Member of the Month

Devtalk Sponsors

Pragmatic Bookshelf

Practical resources that improve the lives of professional developers.

Erlang Solutions

We build trusted fault-tolerant systems that scale to billions of users.

Honeybadger

Real-time error tracking, performance insights, and observability for devs.

EEF

Supporting innovation across the BEAM ecosystem.

coders51

We build reliable cloud platforms for business-critical systems.

Manning Publications

Develop your skills with books, videos, and courses.

AppSignal

Catch errors, track performance, monitor hosts and more.

WyeWorks

Enabling companies to succeed by building software people love.

Pragmatic Studio

Courses that move you from confusion to "Aha, now I get it!"

Linux New Media

Publishing Linux Magazine, ADMIN, and MakerSpace for 25+ years.

View all our sponsors ❯

Categories:

Sub Categories:

Popular Portals

Devtalk Sponsors

Pragmatic Bookshelf

Practical resources that improve the lives of professional developers.

Erlang Solutions

We build trusted fault-tolerant systems that scale to billions of users.

Honeybadger

Real-time error tracking, performance insights, and observability for devs.

EEF

Supporting innovation across the BEAM ecosystem.

coders51

We build reliable cloud platforms for business-critical systems.

Manning Publications

Develop your skills with books, videos, and courses.

AppSignal

Catch errors, track performance, monitor hosts and more.

WyeWorks

Enabling companies to succeed by building software people love.

Pragmatic Studio

Courses that move you from confusion to "Aha, now I get it!"

Linux New Media

Publishing Linux Magazine, ADMIN, and MakerSpace for 25+ years.

View all our sponsors ❯

We're in Beta

About us Mission Statement See our Roadmap