I sincerely hope this is satire (it sure is very HN in nature). "AI" in its current generative incarnation is prone to hallucinations/confabulations that cannot be avoided. In what world is that compatible with a job where a mistake can kill hundreds of people a few minutes or seconds later?
Yes, non-commercial planes crash far, FAR more often than commercial flights, at the tune of about 200-300 fatalities a year, you can play with the data a bit here:
It was reported because of the prior incident in DC. Also this crash was more newsworthy because it was damaging to ground structures and there were bystanders on the ground who were injured.
Can nostr be used for the same form of social network as bluesky (ie, a twitter clone)? It seems that it would only show messages from people the user explicitly follows, for example, and not replies by a third user.
Also it's distasteful to do any sort of content addressing on json data. One would think they'd learn and use CBOR after seeing secure scuttlebutt, but no? Now you have to worry about only sending text payloads, escaping some characters, avoiding whitespace when printing the json... Guaranteed to be a source of bugs...
1) It's up to the relay and the software how much of the firehose of posts to present to users. Your client is in control if whether you see posts from your follows (who you follow), or the entire world.
2) One of the things Nostr did get [slightly] wrong was the hashing of the JSON. It's pretty straight-forward to sort properties, and remove spaces, to create canonical JSON that can easily be hashed, but (and I forgot the specific reason) Nostr made it where you can't directly store Nostr in IPFS (for example) and have the post hash/ID be identical to the IPFS CID of the canonical JSON. They missed that opportunity because fiatjaf was not well enough versed in IPFS, so he got that a bit wrong.
All that being said I am still a fan of Nostr. It is far better than other Social Media protocols imo.
I think they should have not reinvented the wheel ;-) and use dCBOR42, which has an actual canonical form. But somehow people like to use json in places where it's shown again and again it's a terrible choice.
The problem with CBOR is that once people relate it to IPFS their will be massive push-back, because IPFS is seen as too complex. I know this is true because I saw it happen. To these kids even XML is deemed "too complex", thus their love affair with JSON instead.
The reason Social Media protocols need to be kept simple is precisely for this reason. Getting developers to all agree on things is next to impossible. So the way to combat that is by removing all those "things", and go with the simplest design that's workable. It's almost like politics in that it's "The Art of the Possible". And to be "possible" in this context means universal acceptance.
Maybe you're right, that's quite sad. I found dasl.ing to be quite nice and simple as a foundation for dCBOR42, without needing the full ipfs craziness. Oh well.
ok. And you're right too that CBOR is the "correct" thing to use (despite what I said about acceptance), if we wanted to do it right. CBOR could be the only "complex" piece. Everything else could be Nostr-like (i.e. simple, and using relays).
A paper passport can be valid for 10 years (maybe more, I'm not sure). It can be stashed in a safe. It can be left alone for several years and be picked up just before leaving for the airport.
A smartphone will not satisfy any of these properties.
It's not "obviously" typed. Values in python have (runtime) types, sure. But contrast that with a statically typed language in which expressions (and functions) have types. Expressions in python do not have types at all (at least before annotations were added).
There's absolutely a constructivist form of unification, the description of a particular unification algorithm is typically a rewrite system (OP has one here: https://www.philipzucker.com/assets/traat/unify_rules.png) which qualifies as constructive imho (it builds an explicit solution, ie a substitution). But the imperative implementation of such a rewrite system can be readable too (especially if you still have pattern matching as in, say, Rust or OCaml).
I don't think there's any link to be had with the Curry Howard correspondence here. No types, no lambda calculus, nothing of the sort.
When I was saying 'easier' if we chose to do logic inside a theory using the Curry-Howard correspondence then we find out that it is intuitionistic, and as you mentioned 'proofs' that means it may be important to you vs. someone who is say using lambda calculus as just a programing language.
The Curry-Howard correspondence results in an isomorphism 'Programs'(Haskel Functions) and intuitional proof systems, if you assume they are traditional proofs internally you will have a bad time.
What is important is what we lose in respect to what we often assume due to the typical conventions.
Note that this has been a popular resource to introduce the concepts for a while, and I was encouraging you to mostly learn the tradoffs of call/cc to help on that path and avoid globals, not that it is the only or even good solution.
> This course is an introduction to the research trying to connect the proof theory of classical logic and computer science. We omit important and standard
topics, among them the connection between the computational interpretation
of classical logic and the programming operator callcc.
Grounding and negation as failure are also popular, especially with ML which under the VC dimensionality interpretation of learnability is still a choice function due to the set shattering.
I want to disagree, but honestly the recursive method I tend to use is almost isomorphic to a loop + stack/deque. Eager elimination of `x=t` pairs, or eager normalization of substitutions sounds potentially inefficient, imho it's better to check that on the fly upon selecting a pair.
Janet is nice, but the ecosystem is too small. I’ve actually uninstalled it from my Macs recently because I ended up not using it, whereas I can take any C and Lua library and do something with Fennel.
The only real issue with Fennel is luarocks—the experience of adding new libraries (or general dependency management) to a (Lua) project is still gnarly.
Janet has a way to break into REPL, but AFAIK no way to restart (a la condition system).
Fennel has something a bit more robust (assert-repl) and it can restart, but can only return a single value from the REPL, which often creates more errors downstream.
It's been a couple years but I think janet has the primitives for this in the netrepl module which I think is part of the standard library. I remember being really surprised at how much introspection and control over the env when you responded to a repl connection, just at that time no one had put it together into what you want. I also seem to remember the actual janet repl being a different implementation which always seemed weird to me.
Yeah that standard lib extension has always been extremely underdocumented.
I thought I remembered being able to manipulate the env as a dynamic which I think could get you what you need. But reading the source now I guess not? I'm pretty out of practice reading janet.
OCaml might be built with makefiles, but it's also not an easy path at all. Adding a module to the compiler or stdlib is really not straightforward compared to what it'd be with dune (you have to list your new file somewhere, regenerate dependencies, order matters in obscure ways, etc.). To be clear, OCaml is a special project since it also has to solve bootstrapping issues, but still, it's not an argument for "makefiles just work". Dune works extremely well for pure OCaml projects.
Some industries, like agriculture or restaurants, rely so heavily on cheap immigrant labor that enforcing this would cause an economic crash and food prices would soar. Other industries will ask prospective employees their SSN, which illegal immigrants don't have. So, which part do you wish to change?
You're saying the only way for America, basically the richest nation in the history of the world, to produce food is to rely on illegally paying and exploiting foreigners? How do all the other less rich countries make food then?
Illegal immigrants have many methods of getting SSNs. Like, it's not even difficult.
I'm saying that it's force massive changes, and, really, increase prices significantly (food is more expensive in Europe for example). Same in restaurants, you'd have far less staff.
It's not impossible but it'd have to go with cultural changes, and have a dire impact on poor people. Just because the US is rich doesn't mean it's working well, just look at healthcare and how costly and unfair it is.
