The main difference that Denuvo does nothing to improve the experience of the end user.
I don't like Anti-Cheat solutions with elevated privileges but they have (at least for some time) reduced the number of Cheaters in games like Valorant or BF, for most users this is at least a somewhat understandable tradeoff. Denuvo on the other hand is DRM and a pure tradeoff in favor of the publisher at the cost of the consumed.
Isabelle/HOL as a language is nice, but the tooling has deep flaws even outside the pure desktop-first app approach.
The language is different (not necessarily better) in comparison to Lean, but I do agree with some of the points on dependent types. It seems both languages mostly just made different tradeoffs, which imo, were fair and have shaped them into quite efficient tools for their domains. The domain of "proofs" is large and different paradigms just have different strengths/weaknesses, Lean just specialized for a different part of this space.
Sledgehammer is nice but probably just a question of time until an equivalent can be ported/created for Lean. It might also be nice to use for explorative phases but is a resource hog, it also makes proofs concise but I would usually rather see the full chain of steps directly for a proof in the published code instead of a semi-magic "by sledgehammer".
Working on Isabelle itself however is painful (especially communicating with developers) in comparison to Lean. Things like "we don't have bugs just unexpected behaviour" on the mailing list just seems childish/unprofessional. The callout to RAM consumption of Lean and related systems is also a bit of joke when looking at Isabelle's gluttony for RAM.
> but I would usually rather see the full chain of steps directly for a proof in the published code instead of a semi-magic "by sledgehammer".
One issue with this is that coming up with a quickly-checkable certificate for UNSAT is not exactly a trivial problem. It's effectively the same as writing a formal proof.
> Sledgehammer is nice but probably just a question of time until an equivalent can be ported/created for Lean.
I have no knowledge of what sledgehammer is. However...
> it also makes proofs concise but I would usually rather see the full chain of steps directly for a proof in the published code instead of a semi-magic "by sledgehammer"
The goal (ATP) is similar but the idea is a bit different, sledgehammer is not directly learning/applying rules but instead effectively a driver for invoking a bunch of ATPs + SMT solvers at once on a goal in Isabelle/HOL.
It is reasonable to ask for a follow-up project/fork to take a different name. Naming your project, e. G., pgbackrest-ng, does not sound too onerous of a requirement and clearly communicates to users that maintainers have changed (see also paperless ng/ngx as good examples of such a change).
Finding a successor is also not easy nor cheap (in regards to time).
A simple yet almost hard to imemt solution (given the view of an outsider on most U. S. cities respect for bicycles) is to "just" provide actual, hard seperation for the bike lane.
This can done with carve outs/ gaps for public service buses, a somewhat cheap implementation are Pop-Up bikelanes but concrete barriers of 10-15 cm also do the job well.
> Why is it always these efforts are little private things or not for profit initiatives?
Because (relatively) small teams can act faster. It is also a lot easier to have a small, motivated core group with shared objectives and aligned vision of a project. A non-profit/public benefit entity is also a reasonable host for such an effort. Such projects can also tap into public money (under particular circumstances) via the various EU and national grant schemes.
> Just have it be an official EU government backed identity.
The amount of baggage this would entail is quite large. Besides just bureaucracy you almost certainly would then also invite politics even more, because, even for small projects, the next question will be: In what countries is the service hosted and by which agency/developers?
That is besides the almost inevitable inefficiencies for resource usage and other obligations from being associated with public funds (which can require a LOT of internal politics work to acquire and especially retain).
The scope/feature set of both is just quite a lot wider, from IDEs to an ecosystem of 1st and 3rd party libraries and extensions. The rendering engines and their capabilities are also quite different (with Unreal and Unity both being quite a lot more advanced).
Maybe this is just my interpretation but OP effectively argued "too many ineffective meetings, we should have less unnecessary meetings and a clearer, independent direction".
The commenter above argued that the problem was slightly different, it's not too many meetings for communication but too many that are not achieving effective communication. A meeting in itself does not create communication (of information and exchange of opinions etc.) and the commenter wanted to increase the number of meaningful meetings instead of/in addition to just cutting down meetings by numbers. The criticism of not enough time spent on communication is in the same vein, both agree on the issue of "too many unnecessary meetings".
Y'all are saying the same thing over and over with slightly different words proposing that the different way of saying it has a meaningful impact on the message. It doesn't.
>"too many ineffective meetings, we should have less unnecessary meetings and a clearer, independent direction".
>it's not too many meetings for communication but too many that are not achieving effective communication
^^ there's no meaningful distinction between those two, discussions that devolve into such things suck all potential value out of a thread.
The distinction is explicit in the statements you quoted. One is advocating for lessening the number of meetings. One is saying that won't help, and instead advocating for increasing the quality of meetings.
* Acknowledging that too many meetings are ineffective
* Suggesting reducing the number of inneffective meetings
* Saying there needs to be clearer, independent direction
The second is:
* Stating that there are not too many meetings in general (the first says nothing about this)
* Acknowledging that too many meetings are ineffective (same as bullet 1 of the first sentence)
* Not suggesting how to address either problem
I agree with GP. There is no meaningful distinction between the 2, but the first suggests 2 ways to solve the problem of ineffective meetings whereas the second simply acknowledges the existing of problems.
One could reconsider whether building your business on top of a model without owning the core skills to make your product is viable regardless.
A smaller builder might reconsider (re)acquiring relevant skills and applying them. We don't suddenly lose the ability to program (or hire someone to do it) just because an inference provider is available.
Run on premade, static tracks with clearly divided "roads" from the rest of road participants.
Their role is to stop the train in an emergency and adjust to speed etc. to track/driving conditions.
Automating their job probably wouldn't even need the complex ML used for self-driving because the context is significantly simpler and relatively well defined. Maybe a team in city might need such a model but it would still be a significantly simpler task than driving a car.
I don't like Anti-Cheat solutions with elevated privileges but they have (at least for some time) reduced the number of Cheaters in games like Valorant or BF, for most users this is at least a somewhat understandable tradeoff. Denuvo on the other hand is DRM and a pure tradeoff in favor of the publisher at the cost of the consumed.
reply