muldvarp

12 ms·

181.
by muldvarp 3y ago
> So will you admit that the first example has been sufficiently addressed? Because I was commenting on the problem involving the Collatz conjecture. In that this specific program is obviously designed to be extremely hard to prove corre
182.
by muldvarp 3y ago
> It's because we're dealing with an extreme example in which a program's safety depends on the resolution of an open problem. It really isn't. The second example is what a reasonable C programmer would produce if you
183.
by muldvarp 3y ago
> It's the principle of propagating the safety-determining factors of the function that we're stressing That's the main function. It's the function that gets called when the program starts. Where do you want to propag
184.
by muldvarp 3y ago
> The purpose of the prototype is to show the feasibility of the approach we've taken But it doesn't do that. You haven't shown that this approach is able to deal with loops and loops are pretty fundamental to every C prog
185.
by muldvarp 3y ago
> Is it so crazy to claim that this can be replicated for C, without encumbering it with ownership considerations that have no relationship to interface formality? You're not replicating what Rust does, you're replicating what
186.
by muldvarp 3y ago
> I'm simply saying that for the restricted case of safety semantics alone, this deduction can be done. And I'm saying it can't be done, at least not in a fundamentally less tedious and hard way than Frama-C. > Yes, it
187.
by muldvarp 3y ago
> Xr0 annotations seem to be copies of the function bodies, but they aren't actually. You're constantly dodging the question. If annotations aren't copies of function bodies (which is really the only sensible choice), you
188.
by muldvarp 3y ago
> However, the only reason it verifies is we haven't yet implemented `||` You should error on constructs you don't yet support. Not doing so makes it very difficult to ascertain how well Xr0 works. > We could either stop and
189.
by muldvarp 3y ago
> Our argument is that it is the interface formality issue that really determines safety. Frama-C also does "interface formality". Chapter 3 (i.e. the first chapter after the one telling you how to install Frama-C) of the Frama
190.
by muldvarp 3y ago
> We're claiming that the restrictions should concentrate at a different place than where they concentrate in Rust. They should orbit around the interfaces. Rust's restrictions can also be interpreted as restrictions on interfa
191.
by muldvarp 3y ago
> See [0] where our reliance on Dijkstra is transparent. Mentioning that you're vaguely inspired by Dijkstra is not the same as discussing prior art. And it's not like there isn't enough prior art about "safe C"
192.
by muldvarp 3y ago
> there is an extremely strong structural similarity between the implementation and the annotation. If the annotation is basically just a copy of the function body why have any annotation at all? > So it's not at all clear that w
193.
by muldvarp 3y ago
It also can't in general deduce whether the abstract and the implementation match, as doing so would require solving the equivalence problem (which is undecidable for anything as or more powerful than pushdown automata).
194.
by muldvarp 3y ago
> Since we are not academics, I don't see why we're under obligation to do a comprehensive literature review, especially early on. I don't think you're under any obligation, I just think that not discussing prior art
195.
by muldvarp 3y ago
As someone who tried to get Frama-C working on existing code: No, annotating existing code is not much easier than rewriting it. In fact, to make these annotations practical, I had to rewrite parts of the code anyway.
196.
by muldvarp 3y ago
Yeah, this doesn't really do anything for now. It currently doesn't even implement loops. I don't see why I would ever choose this over Frama-C which basically does the same (and is actually battle-tested). I just don't
197.
by muldvarp 3y ago
> That is exactly what is happening, but our sense is that this language will be no more complicated than C itself, and will to a large extent parallel it. The point of interfaces is usually to hide underlying complexity. What's the
198.
by muldvarp 3y ago
> I've been thinking lately that one could probably leverage the same technology to evaluate the quality of research, possibly as a post-hoc verification. I doubt it. They'll be just as effective as ChatGPT-detectors are. Compl
199.
by muldvarp 3y ago
I disagree. LLMs fundamentally change the situation: They make it easier to "write" low quality publications and they make it harder to immediately recognize that a publication is low quality. Before LLMs, one of the main deterren
200.
by muldvarp 3y ago
I wouldn't call it plagiarism, but not even reading the output of the LLM before pasting it into your paper shows a lack of professionalism and indicates that the data in that table might as well be the hallucination of an LLM. Not exa
201.
by muldvarp 3y ago
It doesn't matter whether or not they will join a club. It matters that simply owning (a non-negligible amount of) cannabis is no longer illegal.
202.
by muldvarp 3y ago
I've used MIP, SAT and plenty of other solver technologies and they aren't perfect but I got them to work most of the time. I've never once in my life been able to get a CP solver to solve anything that's even close to a
203.
by muldvarp 3y ago
Do you have any data backing that argument? I could just as well make the argument that Rust has an extensive "correctness above all else" culture that encourages people to thoroughly review pull requests. Without data both of the
204.
by muldvarp 3y ago
If you run somebody else's code and you don't trust that person, you need to read their code carefully anyway. Safe Rust code can do all kinds of shenanigans including: * Wiping your disk * Downloading and running code from the in
205.
by muldvarp 3y ago
You can also just use the Christofides-Serdyukov algorithm. It's fast and it actually has a performance guarantee (it always produces a solution that is at most 1.5 times the length of the optimum).
206.
by muldvarp 3y ago
The entire field of metaheuristics is in dire need of a shakeup. Many of the newer publications are not actually novel [0, 1, 2, 3, 4, 5], the metaphors used to describe these methods only disguise their inner workings and similarities and
207.
by muldvarp 3y ago
> Also anything dealing with finding the minimum distance distances can be short circuited by keeping the shortest distance and not taking paths that exceed that. That's the "bound" part of "branch-and-bound", so
208.
by muldvarp 3y ago
> In other words, this is not practical to solve problems with moderate to large size n. This depends entirely on your definition of "moderate to large". Many real world problems can be solved easily using existing MILP solvers
209.
by muldvarp 3y ago
> I was under the impression that all NP-Complete problems take O(n!). SAT is NP-complete and the naive algorithm ("just try every combination") is O(2^n). Even for TSP there is a dynamic programming approach that takes O(n^2*2
210.
by muldvarp 3y ago
> If it's just carrying on, that sounds bad. Why? If you are an experienced C or C++ programmer you know about these quirks. Replacing an infinite loop without side effects with a crash sounds about as "bad" as optimizing

More ›