Yeah, I also only learned natural deduction, until I got to the languages course and the professor told us “this is similar to natural deduction, but different”.
Personally I don’t like lean, I prefer coq. But that’s mostly the vibes, both are actually fine. Lean doesn’t do constructive logic, it does classic logic, but you have to give up program extraction for that. That’s why mathematicians are head over heels for lean.
*it
Chatgpt is a thing, not a person
Not at all. I would not expect any riir project to reimplement the entire stack in rust. This is not calling a random C dependency. This is literally calling the OS’s API. Literally there’s just this and the kernel.
As you said its goal is to rewrite a C codebase. The C codebase is coreutils. The correct way to getuser is to use the OS’s API, which happens to be inside libc.so, which has nothing to do with coreutils, it’s an entirely different codebase. End of the story.
The OS’s API needs to be exposed as a c library, because c is the only language that can be imported from any other language. If you were to rewrite it in rust, it would use extern 'C' and it could not be any other way. And uutils would still import it from libc.
Maybe one day we’ll see a rust rewrite of libc (tho it doesn’t make much sense), but this has nothing to do with uutils.
If you are asking for a rust wrapper around the correct way to getuser, you have literally posted it. You can find it in uutils.
Also, being compliant is just being compliant. I wouldn’t expect it to be called something like POSIX.rs unless it were implementing every part of POSIX. Which is clearly not what we have here. Or are you suggesting that bash should be called POSIX.c, because it’s in c and it’s POSIX compliant?
Well, if you want to be pedantic, I’ll entertain you a bit more.
You see, C and Unix were “born” together. So sometimes, POSIX intertwines them in weird ways. In this case, getlogin is declared in unistd.h because it’s part of the Unix standard API, however the POSIX standard states that it must be implemented in libc. So the POSIX compliant way to getlogin is to call into libc, which doesn’t need to be glibc, you could use musl and avoid the GNU dependencies. If rust’s stdlib were to offer a getlogin function, the proper approach would be to still call libc. It’s like if on windows you were to call into Win32 to getuser, except on *nix it’s the same file as libc.
If you want to replace the getlogin implementation, the POSIX compliant place to do it is not in coreutils but in libc, like the aforementioned musl library does.
So the key here is that getlogin is not art of the c system API. It is actually part of the POSIX APIs, it is just “located” inside of libc, which by the way, does not need to be GNU if you are concerned with uutils’ philosophy.
I would like to interject for a moment. What you are referring to as coreutils Is actually coreutils+libc+Linux… And fill the rest yourself.
The “anti rust” crowd spends half of their time yapping about how you still need c in some places, then why did you get upset with calling into libc here? Are you suggesting to rewrite every rust program in C so you can have only c calling into c?
I know that’s not what you meant… But those are all digital…
I highly doubt that the birthrate in Italy is 1.14
The government and the media doesn’t stop yapping about how it’s declining and we are going extinct.
This happens of course for economical reasons, and the government comes up with the most half assed “solutions” to ever cross human mind. Like “reduce VAT taxes on diapers and powder milk” like that is gonna make any difference.
I’ll give you a fast-forward of the subjects you need to study to actually learn this stuff (with links). Many of these are part of typical computer science curriculums. However, most will exclude at least some of this to its fullest. Note that it’s a lot of knowledge, you might find it frustrating to just deep dive into it on your own, don’t take it the wrong way, maybe follow an actual course and you will be guided into all of this. Maybe I’ll also try to give a run-down, skipping the preupedeitic knowledge… later… if I have time.
P.s.: to get the general feeling you don’t really need to know all of this tho. Just skim it. And dive deeper if you like it.
Oooooohhh! That’s my field of study!
So, you know how in programming you have data types (like int, float, structs etc…) well, they are actually math.
In math, more specifically in logics, there’s these things called “judgement derivation systems”. They are basically sets of rules that tells you if you can derive a judgement, from a set of hypothetical judgement. The most notorious are sequent calculus and natural deduction. Both are used to determine if a logic formula is consequence of a set of hypothesis.
You see, one day Mr Howard wrote to Mr Curry: “I was working on a type system for lambda calculus, and I noticed it kinda look like natural deduction” and curry answered: “wow, that’s cool, I’ll tell you more, a type system for this other thing kinda looks like combinatory logics” and then they both went “could it be that every type system is actually a logic deduction system, and every logic deduction system is actually a type system?” And this is what modern type theory (and theorem provers) are based on.
Now, formal type systems are often defined as judgement systems. More specifically, they look like sequent calculus, and they use a “context” object, which is often identified with the letter gamma.
deleted by creator
There’s a company that sells “reasonably good” replacement pads for most headphone models, and they include links to tweets and posts of people who bought those pads to prove that they fit properly. I don’t remember the name tho
Well, instead of stealing from the drivers, to give to a corporation, it steals from tourists to give to drivers. I say it’s not good but it’s still less bad
Yeah, we are a bureaucracy machine.
People (especially us) often make fun of how convoluted our bureaucracy is, but this has made us extremely good at paper moving. If any country had a go at being us, they would collapse.
Italy. Because you need a license to be a taxi driver, and a random company cannot hand them out (and the taxi drivers union is powerful and corrupt). And because the government gotta know who is renting a room where, you can’t just go wherever you want without anyone knowing, especially foreigners. Whenever you rent a room in Italy, the owner will take a picture of your ID/passport, and send your data to the local government. Also you gotta pay taxes on the rooms you rent.
It doesn’t have to be like this though.
Here, for example, Uber is not allowed and Airbnbs are regulated
Short side because it’s TV facing (in my living room). Edge seat because I like the arm rest. It would be even better If the arm rest was to the right, but my sofa is a reverse L.
almost all the dialogue was written by an alien
Excellent move, George Lucas
I mean… It’s also easier to login when you have no password, but I don’t see people suggesting that
Yeah, because you don’t know the language