aiono

I am surprised that it didn't get any attention here. I have skimmed the paper, and it seems that they got 1.6x faster with Rust rewrite that is more or less the same code. Both versions are sequential code. And then changed Rust to be parallel and got 5.6x faster. They emphasize that converting to parallel was pretty straightforward because all they did was to change a method to be called. Since rest of it is iterator based code it pretty much worked as is. Only parts required change was sharing state between threads which would lead to bugs unless changed.

Probably there is still a lot of room for improvement if they can avoid mutex and use some lock-free mechanism as well. But I think it's nice to see Rust's promise of speed and safety in a real case.

> And that's not really a knock on Lean - it seems to have some of the better documentation out of the alternatives.

It looks scary but actually all those concepts are really simple and probably things you are already familiar with.

When I was little I was doing this on carpet patterns because they suddenly become 3D. It was very fun. But I never realized it could be used for this purpose.

There is also one other similar funny ability I have: Vibrating my eyes. I can willingly vibrate my eyes. I don't think it's any useful ability as I just see shaky when I do it but it's fun to do in front of people. It scares some of them. There is actually a community about it in Reddit: https://www.reddit.com/r/Eyeshakers/

I doubt that although I agree that it's much more useful when cost of a failure is higher. For example I work in a lab that formalizes requirements and we have real customers that pay us for formalization because they find it useful. Some products are things that a failure could cause injury or even possibly death. But not all systems have that high costs and they still see benefits.

> Get back to me when the formal methods actually generate high quality code that cannot deviate from the spec

That would be useful but there is a fundamental issue: code is too specific. İn formal specification you usually don't specify that detailed but you specify the general behaviour of the system. So usually the specification corresponds to a lot of programs with subtle differences. That's why code a documentation falls short: you don't know what is intentional and what is just a random choice. It's simply too specific to describe high level requirements.

The other way around (verification of program with respect to the specification) can be more feasible to implement.

Yeah I wasn't going to post it if it was shared before. But I am happy that some are happy that it's reposted.

It's been a while since I worked on those systems, but you usually decide on some rules that you refine over time. So they are purely logical decisions that you can formalize. I don't see why it would be hard to specify. I don't mean to specify all up front but one can specify the exact decision procedure that is implemented right now very easily in my experience. Generally you have a state machine representing the process.

This state machine is usually embedded in the code, but code has a lot of noise around the state machine that makes it harder to see the underlying state machine.

I think it's more formalisability than requiring upfront design. For example you may have an insurance claim automation system which you can't design upfront because most insurance providers have unspecified behaviour. But that doesn't mean you can refine your automation system as you get more information from interactions. You would still get the benefit that you ensure not leaving out any cases or not having any contradiction in your system

Thanks, I couldn't find it via Google search on this website for some reason.

I found this article interesting because it shows empirical analysis against the commonly held belief that "errors are more costly the later it's discovered in the software development process" including myself.

> variable renaming definitely conveys a semantic change

I didn't say it doesn't. Renaming is a change and you see it but you don't need to see it in every place that refers to that variable. For them there is simply no semantic change they still reference the same variable.

> At least to me whitespace does convey meaning

Can you give an example? If two programs behave exactly the same how whitespace convey a semantic change?

> order of functions

You can see order changes in a structured diff as well if you want but you don't need to hundreds of line of removal and addition like text diff. You would see only the relevant thing which is reordering.

Plain Text diffing has some obvious drawbacks:

1. If you rearrange your functions you will see a lot of additions and deletions while semantically there is no change in the program. It's just noise.

2. If you rename a variable you don't really have any actual change in places where it is referenced but text diff will again show a lot of noise. But the code references is still the same code.

Where is this data from?

> Why do people think someone else should pay their medical bills?

Health is something you can influence but that you don't have total control. I prefer the world where if I am the unfortunate person at least the society will help me. Having health issues is already bad enough. I am willing to pay some of my money for that purpose. It doesn't impact my quality of life when I pay for someone else's medical bills but if I end up needing that I will benefit from it a lot. So the cost it totally worth IMO.

Nix UX really sucks I agree with that. But it has a very robust core model and is reproducible from the bottom up. Tools like asdf, renv etc. just provide you some binaries. If you need some system libraries installed they don't help with that for example.

Can one provide reproducible dev environment that uses a tool that is not yet in mise registry? Or does one need to wait it to be added into the registry? Also if I want to provide a python runtime that is compiled slightly differently can I do that? Or does it have to be distributed as a precompiled binary?

I agree with that. But that can be attemped to be solved by wrapping Nix with a better UX instead of building something from scratch.

Did you try https://devenv.sh/? It uses Nix under the hood but with an improved DX experience. I haven't used it myself personally since I find Nix good enough but I am curious if you would still choose mise over devenv.

This is already a solved problem with Nix shell (except the task runner part). I don't understand why there are any other alternatives still being developed. Nix supports more packages than any other solution, it's battle tested and cross platform (didn't try on Windows but on Mac OS it works fine). And it's more reproducible than any other package manager.

I don't know what's the point of the post is. Safe unions require compiler work? Sure who objects to that?

I don't think this is a good idea. Because zero value changes when you reorder the fields.

Meaning of union and enum changes based on which programming language terminology you use. Enum of Rust is tagged union of C with compiler support. Enum in C is just basic enum of Rust without any fields. The list goes on like this.

I checked the code. The code validates that values are within the range https://github.com/rusiaaman/color-parser-py/blob/ec739c80ba... but the library it wraps already does validation and a lot more checks (see range check here: https://docs.rs/csscolorparser/latest/src/csscolorparser/par...). So the code generated by AI has unnecessary checks that will never be visited.

Can you link to the source where they state that they want to be profitable in 2029? I am curious.

> Usually, those functions and parameters should have been there.

There is a huge leap here. What is your argument for it?

But this way you don't track what you handled in type level it's only available in runtime. So you are back to untracked errors.

  enum program_state {
    X_W,
    Y_X_W,
    Z,
    W,
    Z_W,
    Z_X_W,
  }

You only have these 6 options. And in this case you can easily use a SAT solver to generate the cases for you so that you don't have to write them by hand.

What is the alternative? And is it really better than encoding into the data type?

Only option I can think of is writing unit tests for each case, which doesn't seem like too much different.

And without type encoding you never sure that invariant always hold. You can always manipulate any options in any part of the program. Then after any modification you have to perform a "sanity check" if options are in a well defined state or not. I don't see how this is better than encoding the invariant into the types.

In this example, is it really the case that all 20 are dependent into each other so you have to combine all of them into a single enum? For the ones that are independent you can keep them as booleans and you should.

Simple, your compiler/type checker/static analyzer/whatever needs to ensure that any value that is not unused gives an error. But you need some sort of static analysis for that. Without type checking you don't do that of course.

For "Errors as values", I agree 100% that it's better then special values or untracked exceptions but I also think that current programming languages lack the features that allow encoding errors as values conveniently. Firstly, there is no composition of errors. If I use a library for a network call and then use another library for a database query, now the possible errors should be the union of the errors that can be returned from the either of the functions. But most practical languages lack the mechanism to do that (except OCaml). One has to define a wrapper type just to encode that particular composition. And it won't work if I want to handle for example Not Found case but not Internal Server Error. I see this is because most statically typed languages have nominal typing and not structural typing. But it is a necessity for pretty much any software otherwise people will just see that tracking errors is too much trouble in terms of composition.