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.

Separately the spec can often have its own properties which can be verified as a means to interrogate its correctness. For example state machines as spec, temporal logic properties and model checking where the state machine is the abstraction for a concrete system. Worth noting that proving state machines are an abstraction of a concrete system is a going research concern though.

That doesn’t guarantee that the spec will be the right one (as you say) but it’s astounding how often just writing it down formally improves the implementation through rigorous thought.