pron

59 ms·

841.
by pron 1y ago
> IFNDR is a catastrophe because it truly does render the entire software without meaning. In the language . I.e. the language assigns no meaning to source the program, which is, indeed, the "catastrophic" impact of UB (or IFN
842.
by pron 1y ago
As I said, UB means that a program has no meaning in the source language. That doesn't change anything I wrote above about the impact of UB. A hardware fault may also make a program meaningless, BTW, yet we all accept that every progra
843.
by pron 1y ago
Yes, that's what UB means - the program loses all meaning and any effect is possible - but the importance of a bug is much more than just its blast radius. We ultimately care not about the language semantics of a bug but its expected l
844.
by pron 1y ago
Eliminating undefined behaviour is a means to an end (reduces problematic bugs, but not all undefined behaviour is equally responsible to such bugs), and it's not a binary thing (virtually all programs need to interact with software wr
845.
by pron 1y ago
> There's no obvious barrier to it It's like saying that there's no barrier to turning lead into gold except for the fact that it's easier to get gold by other means; that's a good thing! The cost of deriving for
846.
by pron 1y ago
Given that Carbon's space is "languages with full interoperability with C++," I don't think D and Zig are in that space. As to "getting it right" - things are not so simple. The emphasis on memory-safety soundn
847.
by pron 1y ago
> That is not the case for the TLA+ spec and your 1MLOC Java Database. That is the case. Of course, nobody bothers to write the TLA+ proof that that is the case, because even if somebody had the resources to do it, the ROI on doing that
848.
by pron 1y ago
> formal proofs in general are pretty much inexistent in enterprise, unless there are legal requirements to do otherwise. Formal proofs are rarely used when specifying with TLA+, too, BTW. Writing formal proofs (as you would in Lean) has
849.
by pron 1y ago
But both Dafny and Lean (which are really hard to put in the same category [1]) are used even less than TLA+, and the problem of formally tying a spec to code exists only when you specify at a level that's much higher than the code, wh
850.
by pron 1y ago
Programmers (and I'm including myself here) often go to great lengths to not think, to the point of working (with or without a coding assistant) for hours in the hope of avoiding one hour of thinking. What's the saying? "An h
851.
by pron 1y ago
More like 300x if you count working hours. Although I've yet to see anything that would take a person a few days (assuming the task is worth spending a few dats on) and that an LLM could do in six minutes, even with human assistance.
852.
by pron 1y ago
TLA+ was specifically designed for practitioners ( https://lamport.azurewebsites.net/tla/book.html ), although he did use earlier incarnations of TLA to analyse his own concurrent and distributed algorithms. His paper ex
853.
by pron 1y ago
You can read more about the Temporal Logic of Actions in my post here: https://pron.github.io/posts/tlaplus_part3
854.
by pron 1y ago
> I was just contrasting the way TFA explained specifications as being definitions of groups of acceptable execution traces (perhaps checked using a model checker) with Dijkstra’s approach of characterizing the acceptable behavior withou
855.
by pron 1y ago
P.S. A model checker doesn't imply anything about the kind of the formal specification used. It is a program that checks whether all assignments of free variables in a formula are satisfying assignments, or "models" for the f
856.
by pron 1y ago
While there is a proof assistant for checking TLA+ proofs and a couple of model checkers for subsets of TLA+, TLA+ itself is no more and no less than a formal language for expressing mathematical formulas that describe dynamical systems. Th
857.
by pron 1y ago
> there have been a number of formal specification tools that have been developed in recent years which use programming-language-like notation, such as FizzBee, P, PlusCal, and Quint. I think these notations are more approachable for pro
858.
by pron 1y ago
If x is a "properly unsigned" byte that has the value 1, what is the value of `x - 2 > 0` and why? The choice of having unsigned types or not is always one of the lesser evil, and in a language where emitting signals directly t
859.
by pron 1y ago
By no means do C or C++ handle unsigned types just fine. In fact, they're widely recognised as a source of problems even by those who think they're useful (when used carefully).
860.
by pron 1y ago
Other than unsigned types for FFI or wire formats (which Java supports just fine) or for bitfields (which Java doesn't have), what do you want unsigned numerics for? The risk of unsigned types (even without the C or C++ issues around m
861.
by pron 1y ago
> I think by "solid" they mean as close to metal as possible A JIT compiler compiles your code to machine code just as an AOT compiler does, so I don't think that's what's meant here (and they don't mean the
862.
by pron 1y ago
> How'd we go from manual memory management languages to Haskell and Go Because that's what's discussed in the article, which discusses Go and Haskell specifically. > In other words, had the Rust program been designed w
863.
by pron 1y ago
Python may be somewhat more popular [1] in terms of number of people using it (partly because a lot of Python programming isn't about shipping software and many Python users aren't professional programmers), but JS, Python, and Ja
864.
by pron 1y ago
> but my understanding is that it was too little too late. Too little too late to be the #1 language of choice for serious server-side software that it is today? The weird thing about Java is that people naturally compare its popularity
865.
by pron 1y ago
> Yeah, and those are also the opposite of "solid" :) So if that's what the author meant by "solid", i.e. few environmental dependencies, then it's not really about "native" or not, but about how t
866.
by pron 1y ago
> But the point is that native, static binaries depend only on the kernel interface Many binaries also depend on shared libraries. > while the other programs also depend on the language runtime that's installed on that OS You can
867.
by pron 1y ago
> And the very point of writing a native program in the first place is to make it feel solid. What does that mean, and what is it about native programs (i.e. programs AOT-compiled to machine code) that makes them feel solid? BTW, such pr
868.
by pron 1y ago
> However it is like having a team of 20 Junior Engineers working. If you know how to steer a group of engineers, then you can create high quality code by reviewing the code. You cannot effectively employ a team of twenty junior develo
869.
by pron 1y ago
In this case, by "arbitrary" I meant anything we would ask of it. But I don't understand why a machine that is able to reliably write code would be unable to reliably design software. Currenly, LLMs do neither, but if we&#x27
870.
by pron 1y ago
I'm not saying it's not impressive or that it doesn't show great promise, but there are clearly challenges, and we don't yet know when or how they'll be solved. From some big LLM fans I've heard that one major

More ›