bbminner

I have long being fascinated by the the field and curious about it on an amature level, i took some basic proof verification and distributed computing classes back in the grad school days, but I'm clearly not an expert in the field by any means. From the article, it seemed like there are plenty of "traps" that i did not even consider - starting from lean hatches like assume(false), expressive power of TLA+ (CTL, ATL), and ofc challenges of tying an real implementation to a proof. To me all three of the above seem challenging enough to deserve their own tools, and i would appreciate smart people putting effort into addressing these rough edges.

Question to you: i can understand how proof verification like z3 or lean requires a special language and an inference engine; given that model checkers like tla+ are mostly about exploring possible program states and checking properties of such states and chains of states, i do not quite understand why it can't be done with a conventional imperative language to express state transitions and invariants - especially an interpreted one like python (esp with continuation support) or a language targeting a vm like wasm where one should be able to snapshot program state?

Actually, I came to comments specifically to praise the inverted bar charts, I've never seen it before, a very intuitive way to communicate lower is better IMHO.

If you have to express your computation using an "array programming DSL" with things like scan and gather anyways - why not opt to use torch/tensorflow/jax or anything else that targets MLIR? An example of writing a relu using an embedded array DSL is really not helping your case either - that's exactly the problem that these other solutions mentioned above are successfully solving for the past ~15y (starting with theano etc). Not sure what this brings to the table - doing that AoT instead of at runtime?

Oh, at least in the post Soviet tradition of oral exams, you are given plenty of time to think and prepare your argument before you start an actual conversation with the examining professor. And if you need to think more during the exam to answer a tricky question, the professor just shifts to talk to another student who is ready to present their case for the time being. So it is less of a public speaking and more of a conversation where you can take a pause to think through an argument, or a proof, or a problem.

Same. The focus on written exams rated blindly and uniformly at the US higher education system always puzzled me. I guess that's the only way to scale things up when you pay professors and teachers living wages?

And there's also parsec.app but only for windows hosts through.

Honestly this is the first time I am seeing this kind of work that i genuinely like. Most fractal and other kinds of self repeating results are not that interesting at all to me.

How difficult it is to get a perfect beam in practice? Can one manufacture a flat rotman lense like that to introduce sinc phase shifts - this should yield a well behaved very directed beam? What are the practical challenges in doing so?

If AI can find new proofs for well posed math problems, i see no reason why it shouldn't be able to implement a more performant fully featured version of an existing interpreter (eg with JIT and AOT) that emulates python api well and passes all python tests and tests of other projects. It is true that a lot of human effort and thought has been put into squeezing performance out of the existing implementation. It is true that many people have found that getting that last 1% of python test suite to pass turned out to be insurmountably hard. Same is true for math, and yet AI sometimes finds simple solutions that we somehow missed. Maybe there's a simple optimization that was used in an obscure interpreter of a domain specific language that we never heard of. Worth a shot in my mind. If that turns out to be successful, we should ideally find the code that served "as an inspiration" if any.

It might make more practical sense to start from CPython and try to optimize that further though. It even has a "not fully fleshed out" JIT already.

I have not looked into this specific issue, but are we sure that a regression here could have been avoided via a localized test? Maybe issues seem to arise from A implementing a feature with tests. B seeing that A lacks some functionality and adding it (potentially with tests), C seeing this (extra) functionality in A, and using in unintended ways not covered by tests (or in an unintended environment) + multiply by many layers of this A-B-C story up and down the stack.

I agree re Rust vs C - this is not (only) a language issue. What would (roughly) the invariant be here?

In another thread comment below i argue that maybe the system (OS) itself is so complex that it lacks clear contract / the contract evolves too quickly over time (as other parts of the code need to change the given piece of code to extend it to their use case) and that defies clear encoding?

Or we lack easy enough means to describe specs? I tried reading jepsen spec earlier today and despite it being an "integration test" of sorts, it is far from "simple".

Can an entire OS or a system of comparable complexity be decomposed into objects simple enough that their entire intended behavior (with all edge cases) can be explained in a paragraph of human text + half a screen of dense behavioral "spec" - if i do X and do Y, Z should come out / hold _no matter what happens in-between_. Or that's what asserts + fuzzing is effectively supposed to do? Is there a clear distinction between invalid input and failed invariant in typical C code? I guess error code vs seg fault?

On the other hand, it is (both halting and spec adherence) are checkable under compute and space constraints though? :) I'd say the biggest hurdle are means to describe the spec in way that is easy enough for a human to produce to make it feasible.

Not a DB person either, but things like TLA+ seem very hard to write even with LLMs. Behavioral tests with an enumerable number of random paths to take (aka model checking - eg jepsen) seem more feasible. Although you can't check internal properties of the system (string `pass` or any of it's copies or parts are not held anywhere in memory at any point between lines A and B) unless we can check that two memory dumps are indistinguishable with different pass strings (assuming we abstracted away storage devices in a test environment).. Also not sure if it's "easy enough" to write such tests either.

Maybe the reason is that OS domain objects / primitives are too complex and not "isolatable" enough / lack a clear contract at all? (Hence multi file refactorings that break invariants.)

+1 that there are few things more exhausting than listening to someone's "proof of work"

i'd rephrase as "visible lack of effort is problematic" - anything above that passes the bar for me, and other factors become critical

I am far from a security expert, but from the number of "we missed a single line C check across files during refactoring" critical security bugs discovered on a regular basis these days, the whole premise of a "giant secure open source C codebase" seems questionable. It is not specific to C of course, but invariants are arguably even harder to enforce and track consistently (esp under changes to code) in C. Unsure if FP with invariants encoded in types is a practically feasible scalable solution either. Model checking? [LLM] fuzzing? Fewer primitives with clear boundaries? Is that how seLinux was "checked"?