Re: [irtf-discuss] Usable formal methods side meeting at IETF 115

[Buday Gergely <[e-mail]>]

Hi Sampo,

you wrote:

11/7/2022 10:06 PM keltezéssel, Sampo Syreeni írta:
> I think English should augment formal specifications as it could 
> ignite debate whether the formalisation is correct and unambigous.
>
> Here I'd go more with the literal programming idea, and coloring your 
> statements with comments. Because if you really formalized your 
> protocol fully, so that the formal description really is whole and 
> binding, there is no need for debate. It just is or isn't valid.

Formal verification can check whether a system conforms a specification. 
But there's always a question whether the specification conforms reality.

You can prove theorems about your definitions with a theorem prover, but 
are your definitions right? This is another type of code review that 
protocol experts should do.

>
> As such English (why not other languages) simply serve to explain to a 
> human, what the intended semantics of the protocol and its data 
> formats are meant to be.

Formal logic does not stand in itself, there are always thoughts about 
the protocol, system etc. that should be expressed in plain English to 
ease understanding. At all, for many formal methods practitioners, the 
main goal of formal verification is to better understand our designs, 
let the computer do the "trivial" stuff.

- Gergely