Indeed, it seems to occupy a middle ground between fast-and-easy AI prompting, and slow-but-robust traditional programming. But it's still relying on AI outputs unconstrained (as far as I can tell) by more formal methods and semantic checks.

But it's also hard for me to grasp the exact value add from the README, or why I should buy their story, so I'm not sure.

Name and shame?

Apologies to the user if they aren't an alt and this is just their genuine first post, but: We really ought to delegitimize the whole "creating alts to post unpopular opinions" trend. I know HN is very privacy-centric, but it just seems wrong to me when someone isn't willing to stake their reputation on (what I charitably assume are) genuinely held controversial opinions.

That's kind of the point - encouraging people to post genuine thoughts that they otherwise wouldn't because of the fear that they might suffer for it later. Sure, it doesn't always encourage the most well thought-out comments, but raising the bar for new commenters with no/low reputation is how you end up with echo chambers.

I think the policy is there for a reason. I think it encourages more free discussion. I don't know if you are upset that there is a way for people to express thoughtful ideas without being bullied for doing wrongthink or havingt he wrong opinions.

I mean I assume it's a bot comment. It has that LLM stink to it in writing style even without the "new account" signal.

A bit uncharitable. I'm a diehard fan of Rocq, but it's nothing unusual to see the young new hotness that is Lean continue to get the spotlight. It's not a sign of Microsoft putting its thumb on the scales, and the hype for Lean has long predated LLMs.

It's certainly less mature when it comes to verified programming, but its appeal to mathematicians (rather than formal methods experts) has earned it much respect.

I don't think he's referring to Lean specifically, but any sort of executable testing methodology. It removes the human in the loop in the confidence assurance story, or at least greatly reduces their labor. You cannot ever get such assurance just by saying, "Well this model seems really smart to me!" At best, you would wind up with AI-Jim.

(One way Lean or Rocq could help you directly, though, would be if you coded your program in it and then compiled it to C via their built-in support for it. Such is very difficult at the moment, however, and in the industry is mostly reserved for low-level, high-consequence systems.)

>Such is very difficult at the moment

What do you mean? It's a nice and simple language. Way easier to get started than OCaml or Haskell for example. And LLMs write programs in Lean4 with ease as well. Only issue is that there are not as many libraries (for software, for math proofs there is plenty).

But for example I worked with Claude Code and implemented a shell + most of unix coreutils in like a couple of hours. Claude did some simple proofs as well, but that part is obvs harder. But when the program is already in Lean4, you can start moving up the verification ladder up piece by piece.

Well, if you do not need to care about performance everything can be extremely simple indeed. Let me show you some data structure in coq/rocq while switching off notations and diplaying low level content.

Require Import String.

Definition hello: string := "Hello world!".

Print hello.

hello = String (Ascii.Ascii false false false true false false true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true true false true true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii true false false false false true false false) EmptyString))))))))))) : string

You know you could just define the verified specs in lean and if performance is a problem, use the lean spec to extract an interface and tests for a more performant language like rust. You could at least in theory use Lean as an orchestrator of verified interfaces.

In Lean, strings are packed arrays of bytes, encoded as UTF-8. Lean is very careful about performance; after all, a self-hosted system that can't generate fast code would not scale.

But isn't that tantamount with "his comment is a complete non-sequitor"?

I don't think so? Lean is formal methods, so it makes sense to discuss the boons of formal and semiformal methods more generally.

I used to think that the only way we would be able to trust AI output would be by leaning heavily into proof-carrying code, but I've come to appreciate the other approaches as well.

But that's exactly my point. "It's natural to discuss the broader category" is doing a lot of heavy lifting here. The blog post is making a very specific claim: that formal proof, checked by Lean's kernel, is qualitatively different from testing, it lets you skip the human review loop entirely. cadamsdotcom's comment rounds that down to "executable specs good, markdown specs bad," which... sure, but that's been the TDD elevator pitch for 20 years.

If someone posted a breakthrough in cryptographic verification and the top comment was "yeah, unit tests are great," we'd all recognize that as missing the point. I don't think it's unrelated, I think it's almost related, which is worse, because it pattern-matches onto agreement while losing the actual insight.

I didn't really read it as a specific advert for this computer, but rather a nostalgic defense of cheap starter PCs in general. It gave me some hope for the future.

`grep -P` kinda annoying. GNU has Perl-compatible regex, and BSD does not. You're reaching for `perl` or installing `ggrep` the moment you need a lookbehind.

BSD grep is the pure grep version though. Perl regex is unnecessary bloat.

Is it unnecessary bloat to match for digits X in patterns $X, say among a bunch of receipts? Eye of the beholder and all, but I'm inclined to think no.

Meetings aren't infrequent for many jobs. As well, small homes may not have the desired desk space for multiple full-time offices.

Sounds like whoever is scheduling meetings need to adapt to a new asynchronous environment whereas many meetings isn't necessary.

I'm not saying everyone must be WFH or that everyone must have a home office. I'm just having hard time imagining how two people cannot WFH in a 1-bedroom apartment. Unless both of them work in a call center.

> Sounds like whoever is scheduling meetings need to adapt to a new asynchronous environment whereas many meetings isn't necessary.

I agree, and a lot of my 'participation' in these meetings these days is read the papers, write my opinion, attach it to the documents and tell people I'm not attending.

That said we're 5 years in to this thing and people haven't adapted.

> The AIs will soon surpass human capability.

The rule can be revised later.

> I'm worried banning AIs altogether will eventually lead to some form of prove-you-are-human verification to use the site, which will reduce anonymity.

Of all the sites on the Web to worry about this happening, HN is low risk. Oppose that change if it comes, not this one.

> And there is a legitimate use for LLM rewrite to counter identification by stylometry

Source for comment-level stylometry ever actually being someone's downfall, despite availing themselves to every other much more standard defense measure? Regardless, if your experimental means of deanonymizing yourself comes at the expense of the site's quality, it is probably not welcome.

"Perfection is achieved, not when there is nothing more to add, but when there is nothing left to take away."

Antoine de Saint-Exupéry

"The greatest ideas are the simplest."

- William Golding