Have I?
Are you arguing with me or the parent who actually called it “sus af”?
1,916 karma · joined March 19, 2014
Are you arguing with me or the parent who actually called it “sus af”?
I can unequivocally claim that Victor receives at least two orders of magnitude more social media engagement, while Lean likely has 4-5 more magnitudes of actual users.
Serious users of Lean simply have no need or reason to star the repository.
The person I am responding to made a SPECIFIC claim when they said, “A complete implementation have been released”
They then ASKED, “how is that not a substantiation?”
Uploading code does NOT substantiate anything.
The code must been executed, tested, analyzed and/or verified in order to substantiate ANYTHING.
We are in limbo because MOST people are JUST seeing the code now. Almost nobody has evaluated it.
BTW, I got the Discord announcement BEFORE I saw the HN announcement (Because I’m not a hater or a bully) and I started looking at the Lean code as well as the TypeScript compiler.
Have YOU been evaluating it? Do you actually have an informed opinion, or are you here to fight the bullies?
Have you evaluated it?
Wouldn’t you be inclined to withhold any claims of anything being substantiated until it’s actually been evaluated?
I think it’s also worth noting that Barry Jay has a particularly strong vantage point for unearthing this particular foundational candidate. First, his advisor was Joachim Lambek, who’s responsible for adding Category Theory in the Curry-Howard-Lambek correspondence.
If one looks at Barry’s body of work over his lifetime, it’s no surprise it would culminate into an elegantly beautiful system capable of self-reflection.
I think his 2025 PEPM paper did a great job explaining the ideas to a regular programmer / wannabe academic like myself: https://github.com/barry-jay-personal/typed_tree_calculus/bl...
Sometimes you want to give certain people an incentive to not be your customers because your company would be entirely better off if they were someone else’s customer.
If your local government doesn’t already employ competent people that can properly regulate and oversee the infrastructure impact of a data center, they will be overwhelmed by experts who know how to steamroll them. Passing a moratorium is the right thing for that community to do because it’s clear their local government isn’t up to the task of keeping a giant corporation (that employs armies of experts) accountable.
It is safer to say no from the outset.
What you might not understand is Loudoun heavily regulates data centers in this area. All infrastructure improvements needed to power and cool the data centers are paid by service providers. The water used to cool our data centers is sourced from our wastewater which goes through a special treatment facility that was funded by the tax revenue from the data centers.
Our property taxes are lower because the tax revenue from the data centers makes up for the difference. We have excellent schools and fantastic recreation facilities.
Oh yeah, our electricity rates and water rates are competitively low too.
I’m not here to champion data centers, nor am I claiming this is what normally happens when a data center is built.
I’m trying to point out that when they are TAXED and REGULATED, they can actually be a boon the local community.
The problem you’re seeing in these other communities are local governments bending over backwards to bring in data centers to the expense of the local population. They’re paying higher rates for water and electricity because the data center wasn’t forced to pay for infrastructure upgrades upfront, so those costs get passed on to the public.
I don’t mind the data centers. I see them every day and walk past them. They don’t emit pollution and they’re quiet and I’m not interested in moving away. I like it here.
Honestly, I don’t think Marty’s “decision” to use generative AI to storyboard will even become a thing that ages.
But let’s say it doesn’t “age well”. What would that mean? Would it mean we’ve turned into a society that looks down on people on using AI tools at ANY stage in a creative process?
Is that where you think we’re going?
Lambda calculus is often the foundation for functional programming languages, but lambda calculus is also a mathematical system you can calculate things with pencil and paper.
What makes lambda calculus interesting is it’s a relatively simple mathematical system where EVERYTHING is defined as a function. I’m serious. Imagine a programming language where you don’t have numbers, bools, if statements, while loops, gotos, etc.
You only have functions. All functions accept one argument (a function) and they always return functions.
Tree calculus is like lambda calculus, but it takes the idea a bit further. Not only can tree calculus do all this stuff where you create functions from other functions, tree calculus is fundamentally capable of reflecting on itself in a way that allows it to easily understand and transform its own interpreter.
In other words, if you base a programming language on tree calculus, your programming language or interpreter will allow you to create programs that can reflect on and transform other programs just like it was any other piece of data.
It’s pretty remarkable, especially when you find out how simple a core tree calculus based language can be implemented.
https://dl.acm.org/doi/pdf/10.1145/3704253.3706138
Tree Calculus is an alternative to lambda calculus that is capable of doing meta-theory without having to construct or bolt on something else entirely.
If lambda calculus provides a theoretical foundation for a language like Lisp. Tree calculus provides a theoretical foundation for a Lisp with a macro system that is fundamentally part of the core calculus.
You don’t have to write parsers and other stuff to do meta programming. It’s fundamentally built in and the paper I posted above explores how to construct type systems as a library, not as something that is outside of the runtime environment.
Here’s what’s really cool about it too: Just like lambda calculus, you can evaluate tree calculus with pencil and paper.
It’s very slick.
Tree Calculus is a novel alternative to lambda calculus as a minimal model of computation. Unlike most minimal systems, tree calculus is fundamentally capable of being fully reflective.
If you were ever interested in creating a programming language that could fully reflect and enhance itself with libraries, this is one of a very few number of known minimal system you can use as a starting point. Think of it as a lambda calculus with macros built into the underlying calculus, not something bolted on afterward based on a partially implemented meta-theory.
If you’re into formal proofs, you can find Rocq proofs of his work in his repo.
https://github.com/barry-jay-personal/tree-calculus
If you’re interested in how something like tree calculus can express a type system, here’s a recent ACM paper:
https://dl.acm.org/doi/pdf/10.1145/3704253.3706138
Personal context, Barry Jay is a respected academic and researcher who’s collaborated with people like Simon Peyton Jones and Eugenio Moggi. His PhD advisor was Joachim Lambek (from the Curry-Howard-Lambek correspondence). He’s not a random professor with a neat toy, Barry’s been working with many of the best minds on the foundations of computation long before most of us knew category theory existed. He’s been formalizing and defining pattern matching, higher-ordered patterns and has been searching/separating what is truly essential from what is not essential for decades.
Seriously, look at his research history on Google Scholar.
I think it will take the rest of us a while to understand and unpack the insight he’s already imbued into such a small and simple calculus.
Our training data is a lot more diverse than an LLMs. We also leverage our senses as a carrier for communicating abstract ideas using audio and visual channels that may or may not be grounded in reality. We have TV shows, video games, programming languages and all sorts of rich and interesting things we can engage with that do not reflect our fundamental reality.
Like LLMs, we can hallucinate while we sleep or we can delude ourselves with untethered ideas, but UNLIKE LLMs, we can steer our own learning corpus. We can train ourselves with our own untethered “hallucinations” or we can render them in art and share them with others so they can include it in their training corpus.
Our hallucinations are often just erroneous models of the world. When we render it into something that has aesthetic appeal, we might call it art.
If the hallucination helps us understand some aspect of something, we call it a conjecture or hypothesis.
We live in a rich world filled with rich training data. We don’t magically anticipate events not in our training data, but we’re also not void of creativity (“hallucinations”) either.
Most of us are stochastic parrots most of the time. We’ve only gotten this far because there are so many of us and we’ve been on this earth for many generations.
Most of us are dazzled and instinctively driven to mimic the ideas that a small minority of people “hallucinate”.
There is no shame in mimicking or being a stochastic parrot. These are critical features that helped our ancestors survive.
I suspect that you are not only ignoring the existing safeguards that have already come of those discussions, but I suspect you’re also ignoring or pretending like those public discussions never happened in the first place.
Furthermore, I suspect you’re also trivializing what is and is not in contention with moral issues as these companies are trying to compete against each other.
I also think you’re probably assuming the slower options are the safer options because you haven’t really considered the risks of ceding power/investment to a less scrupulous competitor.
I’m not claiming any of these men are moral upstanding people or that they’ve done enough.
I think people should be very critical, but they should at least make the effort to ENGAGE in the moral issues and consequences.
Your cheap four word response only adds cheap rhetoric to the conversation.
If you really care about the moral issues, start typing.
Dafny’s expressiveness tends to be more in the service of coherent specifications and less in the service of language abstraction for its own sake.
On the other hand, I think there might be a way to solve this problem for live anonymous chat in a way that doesn’t rely on threats of “punishment” or “banning”.
I think most people looking at this problem don’t appreciate how much realtime information can be calculated from the event stream and how that information can be leveraged toward solving it in near realtime.
While I’m not the kind of person who races to test the most triggering racial slurs, I’m actually glad Anon Pond Heron did because I thought his behavior was informative, especially as you could watch him slowly type out the beginnings of a slur.
I actually think these types of CRDTs can be enhanced with a handful of simple mechanisms to ensure a higher quality chat experience.
I actually think one can make it work, one simply needs to account for moderation and flooding upfront.
The first feature you need is a way to instantly ignore people who are ruining the collective experience. I would think when a person is ignored by a certain threshold of people, their content should automatically be moderated.
The second feature that’s needed is some sort of flood protection or detection. If a user is pasting or trying to flood the chat with characters, they should be instantly hidden and their content be subject to moderation. Being able to distinguish between copying and pasting on occasion and flooding goes a long way.
Included in that same dataset are assaults and sports related injuries, which are additional risky activities.
You might argue assaults aren’t voluntary. My personal experience suggests most assaults are the result of voluntary activity rather than involuntary activity, YMMV.
I’m not being naive. I have lived in a 3rd world country where it wasn’t uncommon to see a family of 5 on a motorcycle.
I would note that you will tend to see, proportionately speaking, more women on motorcycles in those countries for the reasons you suggested.
The OP didn’t say all of the reasons for male related injuries were needless, but if you look at the list, it’s dominated by activities that are inherently voluntary and risky.
I wouldn't call it "building a city", but if you look at Northern Virginia today, you'll find that vertical districts are popping up along the Silver Line metro that now extends past Dulles airport.
At the end of the metro, there is literally a "town center" residential area on one side with buildings around 5 stories tall. On the other side of the tracks is literally fields, but the roads have been laid out like Sim City with empty plots and developers are now beginning to construct buildings starting from the outside perimeter first, working their way toward the metro station.
Throughout the DC suburbs, you will find densely populated areas with relatively tall vertical buildings (15-20 stories) that simply were not there 20 years ago. Reston is a good example. I've watched 4-6 buildings (over 10 stories) get built in Reston alone. They mostly started when the the metro line was finished.
Who writes Lean code in the actual paper but doesn't create a repo or even a username?
Another response is to come to terms with a possibly meaningless and Sisyphean reality and to keep pushing the boulder (that you care about) up the hill anyway.
I’m glad the poster is concerned and/or disillusioned about the hype, hyperbole and deception associated with this type of research.
It suggests he still cares.
Or are you suggesting that the majority of programmers struggle to read and understand fluent method chaining?
I don’t have a dog in this fight because this blog post is very novice oriented. I’m just genuinely confused why you think it’s unreadable or “clunky”. What is it about the fluent example that you find clunky?
Writing your own LINQ provider is a very niche activity done by people who want to translate or “transpile” C# expression trees into something else.
It is fundamentally a difficult endeavor because you’re trying to construct a mapping between two languages AND you’re trying to do it in a way that produces efficient target code/query AND you’re trying to do that in a way that has reasonable runtime efficiency.
Granted, on top of that, I’m sure LINQ provider SDKs probably add their own complexity, but this isn’t an activity that C# developers typically encourage.
I'm more familiar with Alloy, which is a great tool for exploring a specification and looking for counter-examples that violate your specification.
AFAIK, none of the languages you listed above work well in conceptualization phase. Are any of them capable of synthesizing counter-examples out of the box? (Aside: I feel like Lean's meta capabilities could be leveraged to do this.)
I honestly found the article to be an insufferably glib and swaggering piece that was written to maximize engagement rather than to engage the subject seriously.
The author clearly values maximizing perceived value with the least amount of effort.
Frankly, I’m tired of reading articles by people who can’t be bothered to present the arguments of the people they’re disagreeing with honestly and I just gave up halfway reading it because it was so grating.