- suspended_stateCareful, HN isn't your average IRC channel.
- > A formally verified program can still have bugs, because the spec (which requires specialized skills to read and understand) may not satisfy the intent of the requirements in some way.
That's not a bug, that's a misunderstanding, or at least an error of translation from natural language to formal language.
Edit:
I agree that one can categorize incorrect program behavior as a bug (apparently there's such a thing as "behavioral bug"), but to me it seems to be a misnomer.
I also agree that it's difficult to tell that to a customer when their expectations aren't met.
- I think it does indeed make a lot of sense in the particular example given.
But what if we add 2 extra nodes: n5 dependent on n2 alone, and n6 dependent on n3 alone? Should we keep n2 and n3 separate and split n4, or should we merge n2 and n3 and keep n4, or should we keep the topology as it is?
The same sort of problem arises in a class inheritance graph: it would make sense to merge classes n2 and n3 if n4 is the only class inheriting from it, but if you add more nodes, then the simplification might not be possible anymore.
- Your comment is funny, but please note: it's not drawing a pelican riding a bike, it's describing in SVG a pelican riding a bike. Your candidate would at least displays some knowledge of the SVG specs.
- I don't know what GP meant, but I can give an example of how I understand it (disregarding the spurious "the" in his comment): in a type system with sub-typing, your expression could be statically typed to return a certain type, and at runtime return any of its sub-types.
For instance, in typescript you could ascribe an expression with the type Any, yet the actual runtime type will not be Any, it will be any concrete type.
In object oriented languages, you may define a hierarchy of classes, say with "Car" and "Truck" being sub-classes of "Vehicle", each having a concrete implementation, and have an expression returning either a "Car" or a "Truck", or maybe even a "Vehicle". This expression will be statically typed as returning a "Vehicle", yet the dynamic type of the returned value will not necessary be (exactly) that.
- It is true that it amounts to the same number of words, so why would it look more like a wall of text when the text is narrower? Perhaps it has to do with the number of lines?
- I'm reading it on my computer, and it's perfectly fine; yet, how would it look like on a smartphone?
- Reading through the article, it says:
> Shinwell also consulted AI regarding the copyright, which told him that “I conclude that no code was copied from oxcaml” and gave reasons. Unconvinced, maintainer Gabriel Scherer said “the fact that the tool that produced the code attributes its copyright to a real human is a clear sign that something is an issue.”
This is inaccurate, Mark Shinwell didn't participate to the discussion, and if he somehow consulted AI, it is not mentioned anywhere in the discussion. Actually, the AI analysis was performed by the PR submitter.
The topic of the article has been discussed in another HN submission:
- What forces you to publish this work as a PR, or as many PRs? You could have simply kept that for yourself, since you admitted in the PR discussion that you found it useful. Many people seem to think you haven't properly tested it, so that would also be a good way of testing it before publishing it, wouldn't it?
- I think you need to define what you mean by the term "virality" here, because I don't see how this could be associated with any feature of the GPL, and it's definitely the reason of disagreements in this thread.
- I think you need to define what you mean by the term "virality" here, because I don't see how this could be associated with any feature of the GPL, and it's definitely the reason of disagreements in this thread.
- It's possible that at some point in the past they used TLS, but I believe that MTProto(0) is used now for any communication through Telegram.
- I don't understand the last line in your comment: if Telegram doesn't have good encryption, why would anyone require to have a backdoor installed? Are you implying that the French government isn't able to decrypt a bad encryption scheme? Or that the idea that this government asked for a backdoor is preposterous?
- But metadata is data too, right? I guess the next question is, would it be possible for parts of the FS metadata to remain untouched for a time long enough for the SSD data corruption process to occur.
- Or they got inspired by how this is done in OCaml, which was the host language for the earliest versions of Rust. Actually, this is a behaviour found in many FP languages. Regarding OCaml, there was even a experimental version of the REPL where one could access the different variables carrying the same name using an ad-hoc syntax.
- > On a separate point but equally important, I don't understand why sh scripts are exempt fom unit tests.
Likely because:
- it's an older culture than unit testing
- people write shell scripts for one shot tasks, or to automate tasks which are system setup/configuration specific
- if a shell script becomes useful enough, it gets rewritten in a more apt language
- That's Point-free style programming.
- https://chat.mistral.ai/chat/12da2e83-f3f1-4a47-b432-753cac2...
I suspect they chose that name because of the proximity with the word "cloud".