Hacker Newsnew | past | comments | ask | show | jobs | submit | reddit_clone's commentslogin

I am still wondering about the effectiveness of using grep/awk (and ad-hoc python scripts) in code bases, as opposed to more sophisticated LSP and the like?

This is very interesting.

I am new to Rust and also new to formal verification.

Can someone ELI5 this for me?

(Also, when does the proof happen? During compilation or by running extra tests during unit testing?)


Proof happens before compilation, and doesn't require compilation. You can follow the Verus tutorials for the specifics, but you can use it as a standalone verifier or as a compilation "stage" where it'll run its verification and then conditionally continue on to compilation.

Their tutorial seems ok: https://verus-lang.github.io/verus/guide/overview.html

But if you want a more complete tutorial on this concept using similar tools (so what you learn from them will transfer well to Verus, even if you need to learn Verus or Rust specific details) check out Dafny or SPARK/Ada. The latter is mature and used in some parts of the software industry today. The former, I don't know if anyone actually uses it in production though theoretically you can (it generates code in several languages, I have not used it for that myself, just in an instructional capacity).


There is a big difference in there I think.

'for' loop is mutating.

Using 'reduce', you can do the same functionally. In some (somewhat) purely functional languages, there is no choice.


Talking about un-guessable, misleading function names,

C++ std::remove.

I would never have guessed what it does exactly. (It moves elements that match the filter to the front, and moves the end-marker forward. Leaves all the elements in the collection. You need to erase them yourself. )


It returns the new end marker

Oh it's a bit like unordered-delete when using an arena. I guess I would have expected an ordered-delete instead

Have you tried other 3rd party terminal applications? (Iterm, ghostel, CMux)

They have many quality of life improvements over the basic terminal.


I use Ghostty. I’ve tried iterm and cmux.

I think we can do better. It’s a hard problem, admittedly. But important.


I'm sure you've considered and rejected tmux, but is this only because it has a different UI than a native OS app?

I do that too. I am trying to use Mise. (Getting interested in Maak. Haven't done anything with it yet. My Scheme is pretty rusty)

Still, Zsh history with fzf fuzzy searching is fantastic. I have years of history I can recall commands with a few keystrokes.

Truly a second-brain.


This does not always work.

Often, the group members presented to, do not have the required knowledge to critique the design document.

I have seen people proposing (demanding even) changes based on vague feelings and their need to be seen as contributing.

Once they say something, it is out there, now it is the poor presenter who has to refute it or accept modifications to the design.


If they don't have the required knowledge before coding, how are they going to have the required knowledge if you skip the design and just hand them the finished code?

Thanks for the WorkTrunk recommendation!

I just installed it and loving it so far.


Unfortunately Chess (unlike Go) doesn't have a good handicap system. When playing without a piece (or two) it is not chess anymore OR it doesn't really matter.. During how many games does Queen's rook come into play during early middle game?

Go, on the other hand has a nice handicap system (which doesn't change the nature of the game too much). One can have a fighting chance against a much stronger player with enough handicap (Upto 9 stones). In Chess terms, an IM can have a _decent_ game against a GM. Probably lose. But the GM has to work for it.


the rook is fairly useless early game (which is why rook and knight odds are surprisingly close), but the queen actually does a lot in the early midgame (just mostly not by moving). The queen is usually keeping a bunch of squares indirectly defended, the trick is that the queen starts in a pretty good position and is much more mobile, so its importance doesn't come from where it is, but where it could be in 2 movies

DOS? Like in MSDOS?

There is something I haven't heard in a long while. Turbo C was the shit back in the day. Until MS came in and pushed Borland out of the way.


To be fair, Borland pushed MS out of the way first, IIRC. Borland was affordable; Microsoft Pascal and C were not. I miss Borland; they did good work.

Borland was huuuge. The name was so prominent, my college-mate one day (without a hint of irony) said: "All this time I thought the first name of Pascal - the mathematician, was Borland and that's how the company got the name. I just learned I was wrong, it's Blaise..."

When Hejlsberg left Borland to work at Microsoft and then made C# and .NET, etc., I followed like a blind, newborn kitten. And then I spent years drinking that kool-aid. I regret this decision to this day. What a waste of my youth.


So long ago, I don't even recall the name.

They had a C++ GUI library, much better than MFC that came later and eclipsed it.

EDIT: Found it. It was called OWL


Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: