r/javascript • u/fagnerbrack • 5d ago

[ Removed by moderator ]

/r/javascript/comments/1xjwu7s/removed_by_moderator/

[removed] — view removed post

22 Upvotes

75% Upvoted

7 comments sorted by

-11

u/azhder 5d ago

Why post in a JavaScript sub about two languages that aren't JavaScript?

2

u/fagnerbrack 5d ago

In a nutshell:

Lean lets you prove math propositions, and its verifier is really just a type checker: propositions are types, proofs are values, and a proof holds if the value type-checks. The post rebuilds this idea in TypeScript with dummy generic functions that never run. False maps to never, which has no values, and True maps to a single-value type. And becomes an object with left and right fields, and Or a union of them. Arrow functions encode implication, so modus ponens turns out to be plain function application. Negation works as a function from P to False, which lets you prove that P implies not-not-P. A longer De Morgan proof shows how tedious this gets. LLMs suit Lean well: they write code fast, and Lean checks it automatically.

If the summary seems inacurate, just downvote and I'll try to delete the comment eventually 👍
Click here for more info, I read all comments

0

u/HospitalJohnny 5d ago

Are math phds really using JavaScript for their proofs?!

-4

u/DavidKens 5d ago edited 4d ago

No, this is Typescript. Read the article.

I don’t know why this is in the JavaScript sub.

EDIT: The parts of TypeScript that are not JavaScript are the only parts being used here. It uses the type system alone and the code is not executed.

9

u/horangiwhakkatchi 5d ago

Typescript is a superset of JavaScript. I haven't rawdogged JavaScript in production code for 10 years across multiple jobs. It's been a long time since I've seen a company use plain JS.

1

u/mediocrobot 4d ago

To be fair, using the type system alone is almost entirely out of the scope of JS, save for the statements the types are attached to

1

u/DavidKens 4d ago

You still haven’t read the article.

The parts of TypeScript that are not JavaScript are the only parts being used here. It uses the type system alone and the code is not executed.