Sometimes I prefer video… But usually not.

E.g. this channel has fantastic videos: https://youtube.com/@therustybits

So glad they made the sane move and fixed std::env::home_dir(). The previous situation of having it deprecated due to fairly insignificant reasons, while recommending an abandoned crate instead was just silly.

Well COBOL hasn’t completely gone away… I don’t think anyone expects C to become completely extinct; just very legacy.

D missed its chance. Zig is clearly going to be the successor to C, for people who don’t want to use Rust.

Yes, but be warned, formal software verification is proper hardcore. Complicated computer science theories, scant documentations - much of which assumes you have a PhD in the field, and in my experience it’s quite a leaky abstraction. You’ll end up needing to know a lot about the actual implementation of Lean to figure out why some things work and others don’t, in a way that you don’t need to in “normal” languages.

It’s quite satisfying when it works though. Like a puzzle.

I highly recommend this fun “game”: https://adam.math.hhu.de/#/g/leanprover-community/nng4

You can transform any recursive algorithm into iterative pretty easily though; just create a manual stack.

The rule definitely makes sense in the context of C code running in space. Unbounded recursion always risks stack overflow, and they probably don’t have any tooling to prove stack depth bounds (you totally can do that, but presumably these standards were written in the 1500s).

Yeah the main reason is performance. In some languages if you use a value “linearly” (i.e. there’s only ever one copy) then functional style updates can get transformed to mutable in-place updates under the hood, but usually it’s seen as a performance optimisation, whereas you often want a performance guarantee.

Koka is kind of an exception, but even there they say:

Note. FBIP is still active research. In particular we’d like to add ways to add annotations to ensure reuse is taking place.

From that point of view it’s quite similar to tail recursion. It’s often viewed as an optional optimisation but often you want it to be guaranteed so some languages have a keyword like become to do that.

Also it’s sometimes easier to write code that uses mutation. It doesn’t always make code icky and hard to debug. I’d say it’s more of a very mild code smell. A code musk, if you like.

I’ve tried to learn Vim in the past but IMO it is not worth it at all. In a world without multiple cursors… sure, maybe. With multiple cursors? No way. I can can edit just as fast as I’ve seen any Vim user do it, and without having to remember a gazillion mnemonics and deal with the silly modal thing.

Multiple cursor editing even has some significant advantages over Vim style, e.g. it’s interactive, so you can do your edit gradually and go back if you make a mistake. Rather than having to write a complex command and only finding out it if works at the end. (If you’ve used regex find & replace you’ll understand that problem.)

I’ll probably get downvoted for this since Vim is kind of a cult, and Vim users get a sense of superiority from it. Kind of like audiophiles - they don’t appreciate it if you tell them their £10k valve amp doesn’t actually sound any better than your £1k digital amp.

For editing on remote computers I use VSCode remote or Micro for quick tasks.

Yeah I just took a look at it. First thing I did was click on the “source” tab on a repo. That actually makes the source tab disappear? Clearly not designed by anyone who has any experience designing sane UI.

I think Gitlab and Forgejo are better options, and not run by a creep. Forgejo is similarly fast and actually has a sane UI. The tabs don’t disappear!

Yeah Verilog. That’s literally the language people use to design chips and FPGA bitstreams.

Someone has already done it: https://github.com/Redcrafter/verilog2factorio

Yeah I think you’ve made it worse than Rust in both cases. They clearly shouldn’t be strings. And the second option is just unnecessarily confusing.