the-lazy-guy

This is absolutely a JIT-compiler. It compiles code into machine code. This is a surprisingly efficient way to get noticeable speedup relative to interpretation. Also it is much safer than proper optimising compiler. Say ebpf jit-compiler functions very similarly, because it is fast and _secure_ way to jit. (well, there's a bit of cheating because before emitting bpf bytecode it goes through gcc/clang pipeline).

LLVM is a large dependency if you need to JIT. There are plenty of smaller (and much faster) alternatives which are much better fit for smaller projects. Larger projects usually roll out their own jit-pipeline because they can integrate better with the source language/interpreter and apply tricks LLVM is not well suited to (say, LLVM is not great at deoptimisation). I think only Julia is really a heavy user of LLVM JIT, also it is known for extremely slow repl from time to time.

Stored and transmitted data also has to be decoded. With modern datacenter hardware bottleneck is often CPU rather than network or disk (SSD). It depends on specific properties of the data. (I used to work on search index implementation which is about decoding and intersecting large amounts of hit-lists; and right SIMD-friendly varint encoding is obviously crucial)

You should use emacsclient, so file will be actually shared. Or better yet - use GUI emacs with its ability to have multiple frames.

While obviously super-impressive, it is clearly not maintanable without AI agent. It has spinel_codegen.rb is 21k lines of code with up to 15 levels of nesting in some methods.

Compilers code was never pretty, but even by those standard, I feel like it is a very-very hard to maintain code by humans.

Fil-C aborts your program if it detects unsafe memory operations. You very much can write code that is not memory safe, it will just crash. Also it has significant runtime cost.

Rust tries to prevent you from writing memory-unsafe code. But it has official ways of overcoming these barriers ("unsafe" keyword, which tells compiler - "trust me bro, I know what I'm doing) and some soundness holes. But beause safety is proven statically by compiler, it is mostly zero-cost. ("Mostly" because some things compiler can't prove and people resort to "unsafe" + runtime checks)

Two orthogonal approaches to safety. You could have Fil-C style runtime checks in Rust, in principle.

> Once you add static linking to the toolchain (in all of its forms) things get really fucking slow.

Could you expand on that, please? Every time you run dynmically linked program, it is linked at runtime. (unless it explicitly avoids linking unneccessary stuff by dlopening things lazily; which pretty much never happens). If it is fine to link on every program launch, linking at build time should not be a problem at all.

If you want to have link time optimization, that's another story. But you absolutely don't have to do that if you care about build speed.

That is exactly what you want to evaluate the thechnology. Not make a buggy commit into softwared not used by nobody and reviewed by an intern. But actually review it by domain professionals, in real world very well-tested project. So they could make an informed decision on where it lacks in capabilities and what needs to be fixed before they try it again.

I doubt that anyone expected to merge any of these PRs. Question is - can the machine solve minor (but non-trivial) issues listed on github in an efficient way with minimal guidance. Current answer is no.

Also, _if_ anything was to be merged, dotnet is dogfooded extensively at Microsoft, so bugs in it are much more likely to be noticed and fixed before you get a stable release on your plate.

It is called experimentation. That is how people evaluate new technology. By trying to do small things with it first. And if it doesn't work well - retrying later, once bigger issues are fixed.

Hot take: CPython is not an important project for Microsoft, and it is not lead by them. The faster CPython project had questionable acheivement on top of that.

Half of Microsoft (especially server-side) still runs on dotnet. And there are no real contributors outside of microsoft. So it is a vital project.

This is Stephen Toub, who is the lead of many important .NET projects. I don't think he is worried about losing job anytime soon.

I think, we should not read too much into it. He is honestly exploring how much this tool can help him to resolve trivial issues. Maybe he was asked to do so by some of his bosses, but unlikely to fear the tool replacing him in the near future.

> A 15,000-line proof is going to have a mistake somewhere.

If this proof is formal, than it is not going to. That is why writing formal proofs is such a PITA, you actually have to specify every little detail, or it doesn't work at all.

> Verifying that those 15,000 lines do what they do doesn't give me much more confidence than thorough unit testing would.

It actually does. Programs written in statically typed languages (with reasonably strong type systems) empirically have less errors than the ones written in dynamically typed languages. Formal verification as done by F* is like static typing on (a lot of) steroids. And HACL has unit tests among other things.

Thank you. These 2 are well-known, as well as plenty others. But I wanted to see answer from the author of the comment to which I replied. Apart from tests (of which both sqlite and curl have plenty, and that is obviously good), I don't see any reasonable difference in sqlite or curl code in aspects which were mentioned in their comment (namely, style and ownership). I'd like to see what they think is reasonable C code.

Can you please provide an example of good C code?

I agree that absence of tests isn't great, and is very common with many C-based projects. But the rest of your comments reads like "ooh, it's C, disgusting!". I hope, I'm wrong.