pron

38 ms·

511.
by pron 10mo ago
But arenas have substantial benefits. They may be one of the few remaining reasons to use a low-level (or "systems programming") language in the first place. Most things are tradeoffs, and the question isn't what you're
512.
by pron 10mo ago
I don't think that a language that was meant to compete with C++ and in 10+ years hasn't captured 10% of C++'s (already diminished) market share could be said to have become "kind of the default" for anything (and c
513.
by pron 10mo ago
> means it's literally impossible for all the big players to achieve this Only because they've achieved that 10% in their first decade or so, but what I said is the case for all languages, big and small alike (and Rust doesn&
514.
Towards Language Model Guided TLA+ Proof Automation(arxiv.org)
4 points by pron 10mo ago|0 comments
515.
by pron 10mo ago
> You mistakenly believe the pattern you've seen is predictive Why mistakenly? I think you're confusing the possibility of breaking a causal trend with the likelihood of doing that. Something is predictive even if it doesn&#x27
516.
by pron 10mo ago
Observing a pattern with a causal explanation - in an environment with selective pressure things spread at a rate proportional to their relative competitive advantage (or relative "fitness") - is nothing at all like retroactively
517.
by pron 10mo ago
Except, as you say, all those factors always exist, so we can compare things against each other. No language to date has grown its market share by a factor of ten at such an advanced age [1]. Despite all the hurdles, successful languages ha
518.
by pron 10mo ago
London doesn't have the income level of Mississippi, although that might be true for the UK average. I'd say that the UK may be "seriously broken", but not more so than other post-industrial countries, including the US (
519.
by pron 10mo ago
The number of domains where low-level languages are required, and that includes C, C++, Rust, and Zig, has gone down over time and continues to do so. All of these languages are rarely chosen when there are viable alternatives (and I say &q
520.
by pron 10mo ago
For all its faults, and it has many (though Rust shares most of them), few programming languages have yielded more value than C++. Maybe only C and Java. Calling C++ software "garbage" is a bonkers exaggeration and a wildly distor
521.
by pron 10mo ago
You're right. My point was that there isn't necessarily a connection between UB-ness and danger, and stuck together two separate arguments: 1. In the context of languages that can have OOB and/or UAF, OOB/UAF are very da
522.
by pron 10mo ago
That's an interesting observation. BTW, I've noticed that when I write in Assembly I tend to have fewer bugs than when I write in C++ (and they tend to be easier to find). That's partly because I'm more careful, but also
523.
by pron 10mo ago
That what happens can be reasoned about in the semantics of the source language as opposed to being UB doesn't necessarily make the problem "a ton more benign". After all, a program written in Assembly has no UB and all of
524.
by pron 10mo ago
> eventually finding a proof using guided search (machines searching for proofs, multiple inference attempts) takes more effort than verifying a proof. Formal verification does not disappear, because communicating a valuable succinct pro
525.
by pron 10mo ago
> Forcing function to avoid use-after-free Doesn't reusing memory effectively allow for use-after-free, only at the progam level (even with a borrow checker)?
526.
by pron 10mo ago
> though an explicit allow of the mockito agent in the jvm arg would have solved for that. You can and should explicitly specify Mockito as an agent in the JVM configuration, as it is one.
527.
by pron 10mo ago
Nothing makes it a massive headache, but I think that Maven/Gradle don't make it as easy as they could and should.
528.
by pron 10mo ago
> Is there a point at which library maintainer feedback would meaningfully influence a by-default JVM change? Of course, but keep in mind that all these changes were and are being done in response to feedback from other users, and we nee
529.
by pron 10mo ago
In September there was a supply-chain attack on NPM where the payload code injected hooks into the DOM API. Changing the behaviour of encapsulated components, like Java's standard library, is not possible now without the application ex
530.
by pron 10mo ago
> To me, it felt like the feature was presented as a done deal because of security. Not security, but integrity, although security (which is the #1 concern of companies relying on a platform responsible for trillions of dollars) is certa
531.
by pron 10mo ago
> They become the arbiter of truth, and so they don't hear the actual truth very often Yes, but they're rarely that stupid. The world sees a man say five times that he's lowered drug prices by 400-1500%. And that was jus
532.
by pron 10mo ago
> right after the next admin renames Dept of War back to DoD It's never actually been renamed. They just changed the stationery and website: https://www.usa.gov/agencies/u-s-department-of-defense . Just like how
533.
by pron 10mo ago
As a non-American living across the pond, the thing that is most terrifying to me about Trump's presidency isn't his authoritarian tendencies, corruption, cruelty, or criminality. The world has seen plenty of leaders like that. Ma
534.
by pron 10mo ago
The "temporal" in TLA+ isn't about □ and ⬦. It's about ' and the abstraction-refinment relation with stuttering at its core (contrasted with o and its non-stuttering meaning). Of course, you can't really specif
535.
by pron 10mo ago
Except it suffices to know that some construction that supports the integer/natural axioms exists without having any specific theorems, such as 1 ∈ 2, about its specifics. In fact, in TLA+, which contains a formalised set theory, the
536.
by pron 10mo ago
I don't think anyone minds this. The purpose of a formal foundation is to prove useful theorems. Junk theorems are just a side effect. But I'm always tickled by logicians who think type theories are philosophically superior to set
537.
by pron 10mo ago
But if LLMs get to the point they're smart enough to deal with the tricker aspects of programming, what makes you think they need help with the easier parts? Conversely, if they're not smart enough to deal with the trickier part
538.
by pron 10mo ago
What I'm trying to say is that a machine that can reliably write a complex, large piece of software and prove its correctness - somethng that, BTW, humans are not currently capable of doing - is also likely a machine that can do that f
539.
by pron 10mo ago
> Perhaps we can start with something "dumber" like Rust or any typed program. If you want to write something correct, or you care about correctness, you should not be using dynamic languages. The most useful and used type of t
540.
by pron 10mo ago
I find this discourse about AI and formal verification of software very confusing. It's like someone saying, let's assume I can somehow get a crane that would lift that vintage car and place it in my 15th floor apartment living ro

More ›