Viewing profile — johnbender

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…

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…

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 be…

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 b…

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 prog…

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…

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 syst…

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.

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 oppos…

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 …

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 dem…

> 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 progr…

There’s decades of research in this vein fwiw, usually referred to as symbolic execution and it’s descendants like concolic execution.

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 syste…

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 cr…

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…

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…

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…

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…

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 …

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 bef…

> 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 …

Raft has been manually verified which was the hurdle here that makes the result interesting: https://github.com/uwplse/verdi-raft

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 a…