johnbender

8 ms·

1.
by johnbender 5d ago
A key problem is that compilation operates on an implicit (compiler writers have this in the back of their heads) notion of correctness which is very roughly “preservation of observable behaviors” where “observable” is sequences of system c
2.
by johnbender 2mo ago
It depends on what “confirmed identical” means. Most compilers (or translators as you like) only guarantee that the output program represents a subset of the behaviors of the input program so it could be that subset is the “safe as in Rust”
3.
by johnbender 6mo ago
I’m confused by the calculus example and I’m hoping someone here can clarify why one can’t state the needed assumptions for roughed out theory that still need to be proven? That is, I’m curious if the critical concern the article is highli
4.
by johnbender 6mo ago
In principle (and we hope in practice) the person is still responsible for the consequences of running the code and so it remains important they can read and understand what has been generated.
5.
by johnbender 7mo ago
You have identified the crux of the problem, just like mathematics writing down the “right” theorem is often half or more of the difficulty. In the case of digital systems it can be much worse because we often have to include many assumptio
6.
by johnbender 7mo ago
Compilers don’t do this error free of course BUT if we want them too we can say what it means for a compiler to be correct very directly _one time_ and have it be done for all programs (see the definition for simulation in the CompCert comp
7.
by johnbender 7mo ago
Sure! The first is an attempt to provide a semantics for activity diagrams as constraints on a state machine and thereby allow folks to specify correctness properties for the state machine using a visual language. Existing work on semantics
8.
by johnbender 7mo ago
FM day job: Interpretation of SysML activity diagrams as temporal logic for use with state machine specifications. Module system for state machine with scoping, ownership type system and attendant theorems to carry proofs of LTL properties
9.
by johnbender 8mo ago
https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/line... Experimental and of course one can debate whether Haskell is mainstream but I figured it merits a mention.
10.
by johnbender 9mo ago
At the outset the article rather bizarrely casts the subject circumstances as a matter of government incompetence in its design and execution of an identification standard as opposed to the reality it then reports on which is DHS tripping o
11.
by johnbender 1y ago
Formal methods like TLA provide the highest value when you have a property of the system that is subtle but should be comprehensive, which is to say you need to know it’s true for all the behaviors of the system. (Aside: this is true even i
12.
by johnbender 1y ago
Minor nit: > The job of a compiler error message is to prove to the user that their code is invalid The job of the compiler error message is to convey why the compiler couldn’t demonstrate the code is correct. The code may be valid but t
13.
by johnbender 1y ago
> Besides, gotta start somewhere. It's probably a PoC, for a platform that will eventually handle all sorts of things. I agree and I think we should give folks leeway to make progress but this seems to be the qualifier for nearly ev
14.
by johnbender 2y ago
There’s decades of research in this vein fwiw, usually referred to as symbolic execution and it’s descendants like concolic execution.
15.
by johnbender 2y ago
A minor point. This is more akin to testing because you’re only checking your formulae against a subset of system traces. Formal methods connotes comprehensive evidence about system behavior. In the case of TLA and similar system that’s a s
16.
by johnbender 3y ago
If you view a file system as running concurrently with another instance of itself where it could be preempted at any time indefinitely and where your algorithm for ensuring your crash protocol invariant must be lock free (two threads helps
17.
by johnbender 4y ago
Fwiw we have at least some reason to hope in this general context that between clever systems work and tightening theoretical bounds via additional assumptions and clever reasoning we might get to practical implementations for some applicat
18.
by johnbender 4y ago
Learning whether the button should change colors is different from actually changing the colors. I agree that the learning part is interesting but at google I suspect those are two different jobs.
19.
by johnbender 4y ago
As an aside Madoff Industries did employ people who earnestly worked outside the Ponzi scheme. I know because I met a few of them when I worked on a database architecture audit for them around 2008.
20.
by johnbender 4y ago
To follow on this sentiment at a slight tangent, I am happy for the enthusiastic attempts from all quarters but folks seem to misunderstand that incremental progress in academia is often due to the problems being very hard. Formal verificat
21.
by johnbender 4y ago
I think this depends on the spec language and the target system. I’ve never encountered a spec more complicated than the program as the goal is always abstraction but I don’t mean to discount your experiences and complexity is affected by t
22.
by johnbender 4y ago
I think this sharply discounts the value of the step before the proof which is writing the specification in a formal language/logic. This often surfaces these misunderstandings before a proof is even necessary. That doesn’t guarantee t
23.
by johnbender 4y ago
> In general you can't prove a program will or won't terminate. As a point of clarity for folks who come to this (the commenter clearly knows this) one can’t _automatically_ prove for an arbitrary program whether or not it term
24.
by johnbender 5y ago
Raft has been manually verified which was the hurdle here that makes the result interesting: https://github.com/uwplse/verdi-raft
25.
by johnbender 5y ago
More likely we’re looking at codesign/correct-by-construction for fully general purpose verification. In many cases it’s possibly to refine a state machine based specification to an imperative implementation (and thereby carry safety p
26.
by johnbender 5y ago
In Coq the user generally writes meta programs to generate proofs as programs at varying levels of automation (Ltac scripts). Here they used IC3 to automatically produce proof that their state based model of paxos satisfies the invariant. I
27.
by johnbender 6y ago
This is an important observation! If the properties of concern for your thread or program are only safety properties (“never does a bad thing”) then the fact that the program may never do anything at all is just fine! Then, if you want some
28.
by johnbender 6y ago
Worth noting that the ISA is more than a set of instructions it’s also a semantics for those instructions. For example the concurrent semantics of ARM processors permits a much larger array of optimizations on the per thread level which is
29.
by johnbender 6y ago
The thing I love most about mechanized proofs is that my questions about the reasoning always have tangible answers, even if the answer is “we axiomatized this thing”. The availability of the intermediate proof state as a part of the publis
30.
Deep Learning’s Climate Change Problem(forbes.com)
1 points by johnbender 6y ago|0 comments

More ›