pron

38 ms·

541.
by pron 10mo ago
But that's why the word "abstraction" is the wrong choice. The ability of a language to express detail and the ability of a language to have high abstractions are two different things, and when we talk about high and low leve
542.
by pron 10mo ago
> Here's a LLM literacy dipstick: ask a peer engineer to read some code they're unfamiliar with. Do they understand it? ... No? Then the LLM won't either. Of course, but the problem is the converse: There are too many situ
543.
by pron 10mo ago
> because there are multiple valid ways of interpreting i There are quantitative ways of describing it, at least on a relative level. "High abstraction" means that interfaces have more possible valid implementations (whether or
544.
by pron 10mo ago
> Where type system complexity entails a tradeoff between the complexity of the language and how powerful the language is in allowing you to define abstractions. I don't think that's right. The level of abstraction is the numbe
545.
by pron 10mo ago
P.S. for the case of computing a mean, I would use Real rather than try to model floating point if the idiosyncracies of a particular FP implementation were important. That means you can't use TLC. In some situations it could suffice t
546.
by pron 11mo ago
> It may sound like executing your specification, but it is a bit smarter, It's more than just "a bit smarter" I would say, and explicit state enumeration is nothing at all like executing a spec/program. For example,
547.
by pron 11mo ago
You say no tools but you can "verify floats" with TLAPS. I don't think that RAM or 64-bit integers have facsimiles in TLA+. They can be described mathematically in TLA+ to whatever level of detail you're interested in (e
548.
by pron 11mo ago
Writing in a language that guarantees termination is not very interesting in itself, as every existing program could automatically be translated into a non-Turing-complete language where the program is proven to terminate, yet behaves exact
549.
by pron 11mo ago
I agree with everything you've said, and about refinements in particular. TLA+ newcomers often think of refinement as an advanced tool, but it's one of the most pragmatic and effective ways to specify. But I'd like to add som
550.
by pron 11mo ago
To make this more constructive, I think that today AI tools are useful when they do things you already know how to do and can assess the quality of the output. So if you know how to read and write a formal specification, LLMs can already he
551.
by pron 11mo ago
You can write proofs in TLA+ about things you don't exectute and have them checked by the TLA+ proof assistant. But the most common aspect of that, which pretty much every TLA+ spec contains is nondeterminism, which is basically the ab
552.
by pron 11mo ago
I'm not sure how a "spec with floats" differs from a spec with networks, RAM, 64-bit integers, multi-level cache, or any computing concept, none of which exists as a primitive in mathematics. A floating point number is a pair
553.
by pron 11mo ago
> You really have to be able to reduce your models to: “at some point in the future, this will happen," or "it will always be true from now on” You really don't. It's not LTL. Abstraction/refinement relations are
554.
by pron 11mo ago
I completely agree it's appealing, I just don't see a reason to assume that an agent will be able to succeed at it and at the same time fail at other things that could make the whole exercise redundant. In other words, I also want
555.
by pron 11mo ago
Maybe in the short term, but that doesn't solve some fundamental problems. Consider, NP problems, problems whose solutions can be easily verified. But that they can all be easily verified does not (as far as we know) mean they can al
556.
by pron 11mo ago
> to me it seems like high-level programming languages are already close to a specification language They are not. The power of rich and succinct specification languages (like TLA+) comes from the ability to succinctly express things tha
557.
by pron 11mo ago
... if it's achievable at all in the near future! But we don't know that. It's just that if we assume AI can do X, why do we assume it cannot, at the same level of capability, also do Y? Maybe the tipping point where it can d
558.
by pron 11mo ago
> it’s not hard to extrapolate and imagine that process becoming fully automated in the next few years. And when that happens, it will totally change the economics of formal verification. There is a problem with this argument similar to
559.
by pron 11mo ago
Occasionally returning wrong results is irresponsible, of course, but how about making deprecated APIs grow gradually slower ?
560.
by pron 11mo ago
No, I mean that instead of vibe coding - i.e. guiding the AI through features - you'll just tell it what you want in broad strokes, e.g. "create a tax filing system that's convenient enough for the average person to use"
561.
by pron 11mo ago
Yes, but perhaps technology can't plateau beyond vibe coding but below "the machine does everything", not because technology doesn't plateau but because that point doesn't exist. Technology could plateau before both
562.
by pron 11mo ago
It's possible , but I don't see any reason to assume that it's more likely that machines will be able to code as well as working programmers yet not be able to come up with requirements or even ideas as well as working PMs
563.
by pron 11mo ago
The thing is that some imagined AI that can reliably produce reliable software will also likely be able to be smart enough to come up with the requirements on its own. If vibe coding is that capable, then even vibe coding itself is redund
564.
by pron 11mo ago
First, the number of projects still on 8 is low, and almost all of them are legacy projects with little to no evolution. Second, modules' encapsulation is not what caused the migration difficulties from 8 to 9+, evidenced by the fact t
565.
by pron 11mo ago
Those of us who were programming in the nineties and before remember there was a lot of competition [1]; not less than today. It's just that not much of it survived to this day in any popular form. Also, C++ didn't have any stro
566.
by pron 11mo ago
Ah, that's a great question, and the answer is in the JEP ( https://openjdk.org/jeps/500#Mutating-final-fields-from-nati... ). When running with -Xcheck:jni, you'll get a warning when trying to mutate a final f
567.
by pron 11mo ago
Tangential: The --enable-native-access option mentioned in the article is part of a large effort we call "Integrity by Default"[1]. The idea is that a library module can violate invariants established by another module (e.g. acces
568.
by pron 11mo ago
That is not, cannot be, and shouldn't be, the bar for peer review. There are two major differences between it and code review: 1. A patch is self-contained and applies to a codebase you have just as much access to as the author. A pape
569.
by pron 11mo ago
Nice, but as of JDK 25 (the preview JEP 445 has become the permanent JEP 512), the canonical Hello World in Java is: void main() { IO.println("Hello World"); }
570.
by pron 11mo ago
I was comparing Rust to the popularity of other languages at the same age . Its adoption rate is not fine for a language that old if it aims to one day be as popular as C++ is today (or even as popular as Go is today).

More ›