Comments URL: https://news.ycombinator.com/item?id=50202217

Points: 348

# Comments: 205

Security properties on the other hand are very often about the relationship between these sequences. For example we like to say that an external observer/attacker can’t distinguish internal state by the external observations (confidentiality) which requires that two observable traces given different hidden values don’t have different observations from the same starting observable state.

If you’re an LTS nerd you know this difference as trace properties vs hyper properties. Compilers try to preserve the former but not the latter.

Separately there is the problem of “what is observable?” For example, if you include timing in your observable behaviors suddenly the kinds of compiler passes that are able to preserve observations tends to zero rather quickly.

In the case of digital systems it can be much worse because we often have to include many assumptions to accommodate the complexity of our models. To use an example from your context, usually one is required to assume some kind of fairness to get anything to go through with systems operating concurrently but many kinds of fairness are not realistic (eg strong fairness).

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 for activity diagrams already exists but doesn’t come with tooling in the way that temporal logic does (https://arxiv.org/pdf/1409.2366)

The second is an attempt to fix a long standing problem with state machine specification languages. While many support composition operators (parallel and/or nesting) none of them come with strong theorems about when temporal properties proven about constituent elements will remain valid in the composite.

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 about individual parts forward after composition.

Experimental and of course one can debate whether Haskell is mainstream but I figured it merits a mention.

With that in mind you don’t have to model your whole system as long as you’re comfortable with the boundaries as assumptions in any property/theorem you prove about it! For example, unconstrained variable in a TLA spec do a reasonable job of modeling an overapproximation of inputs from the outside world, so that’s one boundary you could potentially stop at supposing the your proof can go through in that chaotic context.

> 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 the compiler just can’t prove it (analyses are sound but not complete unless the language is strongly normalizing)

I agree and I think we should give folks leeway to make progress but this seems to be the qualifier for nearly every GenAI demo I’ve seen

Formal methods connotes comprehensive evidence about system behavior. In the case of TLA and similar system that’s a state machine and not the real system but the output for the state machine is a proof that your LTL/CTL/TLA properties hold for all behaviors of the system (traces or trees of traces).

As (maybe weak) evidence the progress on practical implementations of PCPs/SNARGs

https://dl.acm.org/doi/pdf/10.1145/2641562

I agree that the learning part is interesting but at google I suspect those are two different jobs.