itishappy

Note that the Lean kernel itself is not formally verified.

Formal verification of the type system does seem a worthwhile goal, and to my understanding it's something the community has been making progress towards, but I also understand it's still relatively uncommon for most languages.

Is this more an abstract concern over the state of the industry, or is there a specific language you had in mind that you'd prefer Rust was modeled after?

Sounds like you don't have the global privacy control flag set. In Firefox there's a "tell websites not to share or sell my data" flag. In Chrome you need to install an extension (such as an adblocker).

It's simple...

    1. do the tutorial, maybe watch a guide
    2. follow the dedicated onboarding track
    3. give people around you the benefit of the doubt
    4. point things out even if you don't know how to deal with them

Pretty reasonable advice for interacting with others in any capacity. If your jobs haven't provided stuff like this, maybe that reflects more on them.

Agreed, but most people who care about not getting shot in the face aren't giving away guns to their neighbors.

Is amazing compression of information a goal of the universe or of humans attempting to understand the universe?

Also, most models are lossy compression. The heliocentric model is amazing because it is wrong. Complications are simply ignored.

I don't think checking our work is a uniquely human trait. It's our uniquely human traits that made us willfully ignore the better model in favor of increasingly complicated epicycles.

> If we were using [humans] to analyze astronomy, we might just get increasingly complicated epicycles and never realize that the Sun is the real center of the solar system.

> If you are an engineer, how often has an LLM told you (without you explicitly prompting for it): Wait, what you are doing here doesn't really make sense, there exists a much more elegant abstraction that nobody has thought of, let's remove all that code, let's tackle the problem in a different way by thinking from first principles.

I explicitly request it. It's not great at coming up with interesting ideas, but neither am I, and it can sure iterate on them faster than I can...

> A galactic algorithm is an algorithm with record-breaking theoretical (asymptotic) performance, but which is not used due to practical constraints. Typical reasons are that the performance gains only appear for problems that are so large they never occur, or the algorithm's complexity outweighs a relatively small gain in real-world performance. Galactic algorithms were so named by Richard Lipton and Ken Regan, because they will never be used on any data sets on Earth.

https://en.wikipedia.org/wiki/Galactic_algorithm

> If the aim of mathematics is to promote greater human understanding...

Is this the aim of mathematics?

That largely aligns with my view. I think in a large enough codebase (roughly the size QA becomes necessary/relevant) it becomes impossible/infeasible to guarantee correctness. I think the line "clever test suites" highlights the distinction.

In my mind, tests are everyone's responsibility, but the goal differs. A regular developer adds features and should be writing tests to prove their code functions as intended. QA does not add features, so their goal is finding holes in code added by others.

It's the adversarial relationship mentioned by a parent:

> Have [QA] build tests to break the code. Don't give [QA] the job of making a test suite that passes.

Totally agree. My point is simply that this aligns with existing roles.

The QA role (regardless of whether it's performed by an AI or a human) typically involves breaking tests, not writing them. (This applies more to unit tests, integration tests blur this line.)

Yes, "embedded database" is a term-of-art for in-application database. Many (most?) databases run a client-server architecture even for local apps.

> given its propensity to just make shit up and cheat

That's more-or-less how I define QA work. The goal is not proving overall correctness, it's surfacing individual issues.

The article makes a strong point that the slice that needs humans is dwindling quickly. The article seems to suggest our ability to write prose for other humans is our main differentiator.

Emotional responses in threads like these?

I don't think the "drinking water consumed by AI" is a given. Proponents and detractors of AI are both making mutually exclusive claims with confidence. I suspect few if any of the people making these claims have the background to interpret them.

The atom-react module is for interacting with React, and ScopedAtom is for scoping those interactions to specific subtrees, so the entire purpose of this particular example is to avoid passing state through many nested functions. Here's the equivalent React code without Effect:

    import { createContext, useContext, useState } from "react";
    import { renderToStaticMarkup } from "react-dom/server";

    const UserContext = createContext(null);

    function UserProvider({ value, children }) {
      const [name] = useState(value);
      return <UserContext.Provider value={name}>{children}</UserContext.Provider>;
    }

    function UserName() {
      return <span>{useContext(UserContext)}</span>;
    }

    function App() {
      return (
        <UserProvider value="Ada">
          <UserName />
        </UserProvider>
      );
    }

    renderToStaticMarkup(<App />); // => "<span>Ada</span>"

I'd like to learn more about the connection between Zig and Haskell as they seem almost opposite in design and philosophy. I'm pretty sure you just meant they're both "good languages" but if there are parallels I'm missing I'd love to know!

This assumes the goal is to create a productive language.

When I design my own languages (I have written several, all terrible!) it's typically to learn about language design.

Not understanding something is different from it having no meaning.

A library for effects. Algebraic effects, to be more precise.

To be fair "algebraic effects" is part of my priors. If you don't know what that is those specific words won't help you, but the examples should!

Right, you can attempt to take and potentially error, but if you already know that taking is possible you can skip the noise and simply return a result. Checking if your container is empty every time you remove an item is not free.

Shouldn't everybody already know that while using AI to find bugs for oneself is amazingly efficient, using AI to submit bug reports for others is quite the opposite? Burden of verification and all.

NonEmpty is a type that allows you to distinguish between:

    a = [undefined];
    res = a.pop() // undefined

    a = [];
    res = a.pop() // undefined

You wouldn't. Effect isn't an array library.

Console is the very core of what I expect an effect system to need to reimplement.

Console is IO and IO is the effect.

Try it out! Translate a few of the privatives and then see what happens when you try composing a few different ones.

Have you tried reading the big bold text at the top of the page?

> Reliable TypeScript for the AI era

It is a library.

Huh. Still happening. On my desktop too! Works on mobile.