People tell me Lean is really good for functional programming. However, coming from Agda, it feels like a pretty clunky downgrade. They also tell me it's good for tactics, but I've found Coq's tactics more powerful and ergonomic. Maybe these are all baby-duck perceptions. So far, it feels like Lean's main strength isn't being the best at anything, but being decent at everything and having a huge community. I see the point and appeal, but it's saddens me that a bit of the beauty and power are lost in exchange.
My perspective is that network effects are far less long-lasting than they feel in the moment. For example if being decent at everything and having a huge community was the only thing that mattered, Perl would still be a big deal. Many similar examples exist.
In the case of Lean, being the first with a huge library really makes a difference. Just as Perl got a big boost from having CPAN. (Which was an imitation of CTAN, except for a programming language instead of TeX.)
When your library is small, this looks like an insurmountable barrier. But you don't have to match the scale for factors of usability to become more important. And porting mathematical libraries is a good target for LLMs. The source is verified, the target is verifiable, and the reasoning path generally ports.
The flip side of this is that, thanks to LLMs, working on a minority platform isn't the barrier that you might expect. Because if their library can be ported to your platform, then your proof can probably be ported to their platform as well!
> The flip side of this is that, thanks to LLMs, working on a minority platform isn't the barrier that you might expect
This is a nice thought, but with Agda in particular it's just not true. It's one of the few languages I've seen that's sufficiently unrepresented in training data. Frontier LLMs (Codex, Claude Code) reliably say "I realized I can't do this." after wasting lots of tokens going back and forth.
In fact, I think this positions Agda uniquely poorly.
This. LLMs are no good at stuff they haven't seen a lot of training data for (saying this as a SystemVerilog programmer who also does some C-coding for interfacing with SystemVerilog, neither of which has a lot of open source code to show LLMs)
> except for a programming language instead of TeX
TeX is a programming language. It's not a very good programming language, but people have implemented floating-point math [0], regular expressions [1], an Arduino emulator [2], and terminal input/output [3] in pure TeX. The last two examples are obscure, but the first two examples are used (internally) by the vast majority of modern LaTeX documents.
> So far, it feels like Lean's main strength isn't being the best at anything, but being decent at everything and having a huge community. I see the point and appeal, but it's saddens me that a bit of the beauty and power are lost in exchange.
To me that feels like a community that's finally matured enough to start getting on with things. Perfect tools aren't the point; get tools that are good enough and do actual work with them.
You can apply that same argument for the of Python in the ML world. It results in all sorts of pain points that everyone has to deal with all the time.
All large-scale projects are made of mediocre parts. At some point you run out of brilliance and have to structure it so that mediocre can still be a positive contribution.
I prefer agda as proof checker but its not a practical choice for building software. Lean feels like it could legitimately become a successor to Haskell as the go to functional programming language for software development.
I think what holds Agda back from being "practical" is that it just doesn't have good tactics. You can't easily automate proofs and even simplification techniques require some language-level tricks[1]. There's technically support for elaborator reflection (as in Idris) but it's painful and impossible to debug. Certainly nowhere near where Coq and Lean are.
Also true. The slowness is relatively unpredictable, too: sometimes changing a 'rewrite' to a 'with' can increase memory usage tenfold.
While we're at it, another major concern for me is the inscrutability of Agda's error messages. I've had one error message single-handedly overflow my tmux scrollback buffer. There's no way I'm going to be able to interpret that.
> While we're at it, another major concern for me is the inscrutability of Agda's error messages. I've had one error message single-handedly overflow my tmux scrollback buffer. There's no way I'm going to be able to interpret that.
lmao i've been there. Agda is my first choice for proof checker and for math-y explorations but its not gonna be a replacement for Haskell as a production programming language.
I've used agda a tiny bit and Lean somewhat more, and I definitely found it much easier to write functional programs not focused on mathematical proofs in Lean than Agda. IIRC the difference was mostly tooling - Agda's documentation is kind of bad and it's a pain to get it working on your system (and it really wants you to be using Emacs specifically). Whereas Lean documents how to write the cat utility in its own docs and generally has a much better, more modern tooling experience.
I believe you, but this hasn't been my experience. It took me hours to get Lean to work (something odd was happening with the package manager + version + tooling combination). Agda worked out of the box with macOS homebrew. Agda's docs are petty bad, but I've found its cross-linked module documentation incredibly useful. The main issue is knowing something exists.
To be fair, Coq has ProofGeneral and Agda has its emacs mode. Once you go outside these established channels, oftentimes using the tool becomes incredibly difficult. I guess for interactive theorem proving in general you may need some sort of editor at some point.
Yeah, I'm not a fan of the encouragement to use vscode; that said it was pretty easy for me to get neovim set up with Lean tooling, and that's what I use generally.
I'm curious what you like about Agda functional programming? Many of the praises I hear about it have to do with it's dependent pattern matching, and I think Lean suffers a lot more in that regard. I'm curious though if you still find Agda friendlier for "normal" fp (and if so, how?)
Its parameterized modules, extremely elegant yet flexible mixfix notation mechanism, the various niceties around pattern matching (though this one might be a bit of Stockholm syndrome; Agda doesn't nicely allow pattern matching anywhere except at function clauses), the fact that records, GADTS, and modules all feel like aspects of the same thing, and the fact that typeclasses are 'just' records that are automatically filled in. The typeclass and module features IMO already give it some edge over Haskell. I don't know if it's friendlier, but it is more ergonomic.
I think its pretty clear that being too early has been as bad as being too late for most technologies. There are a few that have gradually gained community after decades but it is easier to make a poor copy of one of them and have better momentum and less skepticism.
I suppose it's because the tablet I'm using (reMarkable 2) doesn't have a way to intelligently track what I marked up. Perhaps it's part of their intended design.
This is funny because just a few months ago, I was forced at Heathrow to chug -- not allowed to pour out! -- my entire water bottle that I had filled prior to my flight. The security person watched me do it and added, "bathroom's over there".
Anything a border official says is implicitly backed with the threat of, at a minimum, detention without trial and without basic humane treatment like access to drinking water. Heathrow has well publicised cases (and is not unusual in this).
It's probably much more boring. The choice was likely between leaving the whole water bottle and its contents in a bin of forbidden/discarded items, going home and missing the flight, or chugging it, or arranging a courier for said bottle.
Probably the act of defiance of pouring the contents onto the floor where there was no drain was implied to be disruptive and would have lead to harsher sanction for no reasonable payoff.
As suspected, your claim is grossly exaggerated. You have one blog post from a decade ago (which I remember reading at the time since I met the author at a conference) which is about being denied entry as the grounds for travel were misdeclared, and not about oppressive security theatre at the passenger screening area.
> which is about being denied entry as the grounds for travel were misdeclared
Yes but not really. It's mainly about the kind of treatment you face when you get on the wrong side of the airport machine, and as such it's exactly what you're implicitly threatened with if you step out of line.
Heathrow is a fucking miserable place with spiteful staff and it would not surprise me one bit if someone decided to fuck with a traveller this way. I saw a girl running to catch a bus to another terminal for a connecting flight, and the guy controller her made an enormous stink about her "breathing on me". She was polite and apologetic but she got pulled aside and made to wait for everyone else to get through, got sternly chastised before being allowed to continue (whereupon she missed the connecting bus and presumably her flight). Same trip I saw them them shouting and swearing at disabled travellers who needed wheelchairs. Every other member of staff in the airport was stood around fucking with their phones and seemed furious whenever they had to do their job.
Given that the border officer has discretion to refuse you entry, failing to down your drink can turn into attempting to enter illegally if they want it to.
> If the median UK salary is >£35,000 I really wonder how arrive at the conclusion that missing a flight will set you back "years or decades"...
Ok, now take that figure and deduct tax, housing, food, utilities and so on - how much do you think is disposable/saveable? And then take the typical cost of a last-minute replacement flight and compare those two numbers.
it would be incredibly inconvenient, and maybe missing other parts of a full vacation would set them back, but thats not the only reason people buy flights
It doesn't have to be one or the other. Both ethical consumption and going vegetarian reduce one's environmental impact, and they're independent of one another. So, while someone "truly" optimizing for environmental impact would better spend their time avoiding meat, someone who enjoys meat can still reduce their environmental impact without becoming miserable. Variables like "income" and "environment" are just parts of the equation for the more important heuristic of happiness.
A lot of the activities on that list are like this. Reading the news has a non-zero impact (hey, I'm on HN, and it definitely helps me keep up to date), and it's "easy" in that it fits into my heuristic for happiness. Same with using a metal straw, and same with picking between credit cards.
In a sense, these activities are "free" in terms of their perceived difficulty, but have a positive, if small, impact. If they're "free", why not do them?
It depends where your meat comes from. If you buy meat the way it's produced in the US where you have great big sheds full of cattle in the desert with everything trucked in, then yes.
If you want permaculture, you absolutely must have livestock.
If you want arable farming of any sort, you absolutely must have livestock.
The whole thing breaks down very quickly if you don't have grass and clovers growing in fields, and ruminants eating them, breaking down the tough cellulose, and then shitting it out and trampling it in.
The amount of livestock that we actually would need in that case is probably around 5% of what we actually have (in the US). So it’s still valid if half of all people became vegetarian, and the remaining amount cut their meat consumption to “special occasions only”.
Keep in mind that a lot of our current agriculture is growing feed for livestock as well, so we could cut back on plant farming by a huge amount as well, if we greatly reduced livestock.
> Keep in mind that a lot of our current agriculture is growing feed for livestock as well, so we could cut back on plant farming by a huge amount as well, if we greatly reduced livestock.
Yes and no.
We'd also cut down massively on the amount of food we have available for humans.
What would be better is if people stopped eating soya.
The amount of cattle required to maintain pasture is way fewer than we have right now. From a CO2 perspective factory farmed cattle tends to look a little better than "free-range" mostly due to reduced land use changes (but it is obviously worse from a cruelty perspective). Finally, we can still have farm animals without eating them!!
You might be right, but I was taking that as a given since the article made that claim. I think the general point (of taking smaller actions in lieu of more effective but costly ones) matters more so than the individual "vanity activity".
Right, but I think that was the author's point: many of these activities are seen by their participants as "productive", rather than just "this makes me happy". That was a specific point of the post.
I keep seeing Ghostty in the news, and I've tried it, but it feels like just another terminal emulator to men. This coming from someone who spends 90% of the workday in the terminal.
Asking in good faith -- could someone tell me what's special about Ghostty compared to alternatives?
Zero trolling when I say this: Two things also make it (more) popular on HN: (1) Mitchell Hashimoto (a well respected hacker who got rich, then kept on hacking) and (2) Zig. (Only Rust could attract more attention.)
To me it has a couple advantages over the other options on the market.
1. Feels 'native' and is built for each platform. This means I can use for example familiar right click context menu's and tabs that I find on every other app. I have the option to use the mouse as well as the keyboard which I appreciate.
2. It has sensible defaults with a "Zero Configuration Philosophy" meaning that many of the things I would usually need to fiddle with are already set.
3. It performs comparably to advanced terminal emulators such as kitty.
The combination of all three (and especially the first) is why I use it.
I tried it a few months ago, and didn't perceive any of those items as particular benefits.
1. Terminal emulators that feel 'native' are ubiquitous. Sure, there are also a lot that have idiosyncratic UIs, but I'm not generally using those -- my go-to when working within a GUI environment is xfce4-terminal, which is about as native as I can imagine, given that I'm using XFCE as my primary desktop environment.
2. Sensible defaults may be good for new users, but I already have my terminal emulators configured exactly as I like them, and my benchmark for switching from one tool to another within the same category isn't how welcoming it is to novice users out of the box, it's how easily I can adjust its configuration to match my long-established preferences. The "zero configuration" philosophy is actually a detriment here, as it leads to configurability being obscured to some extent.
3. When I tested it, its performance was worse than xfce4-terminal, both objectively and subjectively. Its memory consumption was higher and it felt laggier in responding to input.
What's an example of a thing you usually need to fiddle with? I feel like 1 and 3 are already true for my existing native terminal emulators, which I also never configure. So presumably there are things Ghostty does that aren't enabled by default on my other ones that I could take advantage of?
I've been using Kitty terminal and they are absolutely comparable in the feature set: GPU-based rendering, speed, customisation. OS-native controls in Ghostty are not very important to me, I like terminal being a terminal, not a GUI.
It's good at what it does. Starts quickly, doesn't get bogged down when dumping large amounts of text into it, got some nice themes.
I find it a bit messy to build but I'm not exactly a compile binaries kind of person anymore so it's probably a good sign that I still manage to figure it out. If stuff like Zig is your thing you'll probably enjoy this part.
My main terminal emulator is the bog slow but reliable Terminator, though in a while I'll probably flip the i3 commands and move over entirely to Ghostty.
Ghostty is quite slow to start on my Linux machine, very close the the first start of GNOME Terminal (or Terminator). Maybe because I'm on Wayland? Are you on X?
I had this issue a few years ago with certain applications and came to find out that it had to do specifically with them using GTK. I googled for it and found the fix, and after all the same apps started practically instantly. Could this be what you're running into?
(I haven't used ghostty so I wouldn't know whether it's actually fast to start up, but what you wrote reminded me about this particular issue.)
Yeah, I'm still on X. I'll make the switch when I haven't heard a friend get really annoyed by something Wayland related in a year or so. It's a Debian system. Not sure if it matters but there's an RTX A500 in the machine.
So, perhaps? For a while I was on a local compile of 1.0.0, and a while ago I started pulling the nightly sources and build from those.
As another person that spends the whole day in the terminal. It's sad to see there is no Windows version. I do not understand why I would need gpu acceleration for a terminal, but I would still try it.
I use a company managed/provided machine that runs windows, I do not have to bother maintaining it. All I use is basically Firefox and a MinGW to have a bash
I used iTerm2 a lot, configured it to my liking, but then I tried Ghostty for curiosity and for some reason I sticked to it. I think it's just cleaner and leaner and the default looks pretty cool and minimalistic, I don't really miss anything from iTerm.
Yes, it's just another terminal emulator, but a pretty solid one that just works.
Their most most recent update replaces all this with a list of recently updated PRs and issues. I've been learning on it heavily since it came out. One of the few recent changes that really feels like a clear improvement.
Whereas when played separately it would be an referred to as an arpeggio. But in harmony we might still refer to it as a chord, as in saying, arpeggiate the C# minor (chord) to start moonlight sonata.
This might better be described as arpeggiating C#m second inversion or even C#m/G# in the right over C# in the left...
This is getting possibly-weird but you could call it an arpeggiation of G#sus4(#5)/C#
I think chords at least three notes played at once, with the exception of maybe power chords. Using your definition, every piece with two or more notes has chords :)
As per my knowledge, and as per Britannica, a chord actually uses three or more notes. A two note structure is called a diad, which implies a bit of confusion in the term "power chord" (written as 5, as in G5, which == G D == 1 5).. as it is not by definition a chord but a diad.
This may be a pedantic clarification, but that is the definition
TBH "definition" depends on the theory from which you're looking at the notes.
In the eyes of the Common Practice two simultaneous notes are not chords; in rock they most definitely are; in EDM you don't even care, since timbre is all that matters; in jazz you'd say "it depends" (e.g. might even be a triad with an omitted 5th... depending on context!)
I've had a reMarkable 2 since 2020 or so. To be honest, the only area of the device I have ever wanted to be hackable was the sync API. I am completely satisfied with the gestures, e-reader and pretty much everything else. But what I'd love to be able to do is to access my files, stored in the cloud, automatically. My use case in particular would be something that passively converts my scribbled annotations into other things.
The API hacking scene is very much dead. Most API implementations have been unmaintained for years now and no longer work. It's a real shame.
This is a strange article to me. I've not seen any class that teaches Prolog place these constraints (use recursion / don't add new predicates) or even accidentally have the outcome of "making prolog look tedious". What's the joke here?
That aside, I wonder if getting the reverse solution (sum(?, 10)) is better served by the straightforward or the tedious approach. I suspect both would work just the same, but I'd be curious if anyone knows otherwise.
It's been a long time since I took a class like this, but I definitely had a similar experience to the author.
Ideas like fold and map where _never_ mentioned in lisp (to exaggerate, every function had to have the recursive implementation with 5 state variables and then a simpler form for the initial call), at no point did higher-order functions or closures make an appearance while rotating a list by 1 and then 2 positions.
The treatment of Prolog was somehow worse. Often the code only made any sense once you reversed what the lecturer was saying, realizing the arrow meant "X given Y" not "X implies Y", at which point, if you could imagine the variables ran "backwards" (unification was not explained) the outcome might start to seem _possible_. I expect the lecturer was as baffled by their presentation as we were.
In general, it left the rest of the class believing quite strongly that languages other than Java were impossible to use and generally a bad move. I may have been relatively bitter in the course evaluation by the end.
Thie irony is palpable. I had the (misfortune) of only being (mis)taught procedural languages by professors who thought computers were big calculators who could never be understood, but could be bent to your will by writing more code and maybe by getting a weird grad student to help.
Patterns might appear to the enlighted on the zeroth or first instance, but even the mortal must notice them after several goes. The magic of lisp is that if you notice yourself doing anything more than once you can go ahead and abstract it out.
Not everything needs to be lifted to functional valhalla of course, but not factoring out e.g. map and filter requires (imho) a wilful ignorance of the sort that no teacher should countenance. I think it's bad professional practise, bad pedagogy, and a bad time overall. I will die on this hill.
Having been on the other side of this (teaching undergrads), I do get why courses would be structured like this. If you actually try explaining multiple things, lots of students freeze up and absorb nothing. Certainly there’s a few motivated and curious students who are three lectures ahead of you, but if you design the class for them, 60% of students will just fail.
So I get why a professor wouldn’t jump in with maps and folds. First, you need to make students solve a simple problem, then another. At the third problem, they might start to notice a pattern - that’s when you say gee your right there must be a better way to do this, and introduce maps and folds. The top 10% of the class will have been rolling their eyes the whole time, thinking well duh this is so boring. But most students seem to need their hand held through this whole process. And today, of course, most students are probably just having LLMs do their homework and REALLY learn nothing
It's existence obviously means some professor didn't allow them to use the standard library and they tongue in cheek show how irritating that is.
I'm sure it's possible they made it up, but we had similar restrictions where I could use an Arduino for my engineering Senior Design Project in college, but no Arduino or module libraries - just our own C. We passed, but barely. It also was weird as it didn't match how normal people would solve the problem.
> Now this is starting to look like Professor of Programming Languages code!
A lot of tier 2/3 CS schools with programming language courses (a survey of multiple languages across various paradigms) teach Prolog this way (and I've seen some fantastically terrible examples of Lisp code coming out of those same courses). It's unfortunate because, at these schools, this is often the only formal course where students branch out of C/Java/C++/C#/Python/JS (and they may only get 2-3 of those over the rest of their courses). It leaves the students with a gross misunderstanding of the languages and dread when they see them again.
>I'm sure it's possible they made it up, but we had similar restrictions where I could use an Arduino for my engineering Senior Design Project in college, but no Arduino or module libraries - just our own C.
When I started compsci, it was the first year of a all-new curriculum for CompSci.
Literally the first week: We had to program an Arduino to play a song on a speaker by toggling GPIO, within a week. No assembly or any of that high-level mumbo-jumbo. We had to read the datasheet, look at the instructions and write the hex representation for each instruction in a txt file.
We had a "linker" tool: It took a basic bootloader (containing some helper functions for GPIO), turned our hex-txt file into actual binary, then just copies that to a set address. The bootloader did nothing more than init the GPIO pins and jump into our code.
We were given the locations of where these helper functions lived, nothing else.
It was to give a quick and intimate understanding of how CPUs actually work and why we use compilers and stuff. It worked really well, but it was so much of a pain that they changed it to allow students to use asm a year or two after.
You were lucky! We had to design and build the computer out of Z80-family components first before we could play around in binary.
There was actually a reason - this was back in '83/84 in a physics lab, and the idea was to be able to build your own logging / control device. PCs existed, but were terribly expensive.
> It also was weird as it didn't match how normal people would solve the problem.
If I can solve a problem by building from preexisting LEGO blocks then I'll probably do that, but it wouldn't be a valuable learning exercise. Students aren't being given problems in need of effective solution, these problems are tools to facilitate understanding.
What you described could be pointless if it made you work on reimplementing trivial stuff that you'd already mastered long time ago instead of focusing on actual problem. Writing your 100th hashmap implementation or yet another I2C driver isn't particularly valuable. Since you mentioned "barely passing", I don't think that was the case though.
It's one of those projects where you never have enough time throughout the year. Coding what we did from scratch wasn't very easy either. I could now probably do the coding in a weekend with the right library code. You learn something either way I guess.
There's nothing wrong with teaching like that. If the class is supposed to teach you something that isn't just "use the stdlib", then it makes sense to ban it.
I'm guessing the author is aware and just venting. It doesn't make it less frustrating though. It's almost like someone asking you to dig a hole with chopsticks.
It reminds me of a satirical post called “Evolution of a Haskell Programmer” in which a nice simple implementation of the Fibonacci function becomes more and more convoluted, abstract, and academic [1].
...is "True" as expected would probably be a pretty interesting exercise if you wanted to be able to get all of the lists. You'd probably need to do an "enumerate the rationals" type of thing, since you need to go to infinity in a couple of different directions at the same time. That is, you can't do nested loops/recursing:
...your life probably gets easier if you limit the domain to positive integers (without zero) since then the list length doesn't diverge. Then a declarative looking solution probably just has a all-modes equivalent to "sort" somewhere within? Certainly interesting to think about.
