> Whenever I read about formal specs it always seems to me like “write the same tests just in a different way”, or worse, “write the same implementation but in a different way”. [...] Can anyone enlighten me?

A big difference is that formal methods allow you to use the "for all" quantifier.

For example, you might write a unit test that says "foo('abc') returns a string with no trailing whitespace".

But with formal methods, you can prove that "for any input x, foo(x) returns a string with no trailing whitespace".

This is a trivial example, but you could imagine something more complicated, such as "for any program P, compile(P) has the same behavior as P".

Of course, you have to define what "has the same behavior as" means!

▲

brap 41 minutes ago | parent [-]

>Of course, you have to define what "has the same behavior as" means

And that's really my issue, for example when you define "has no trailing whitespace", you are basically writing a piece of the implementation. Cover all behaviors, and you have basically re-implemented the function, no?

In other words, if I have the full formal spec of f(), isn't that the same thing as having f()?

▲

chadgpt3 7 minutes ago | parent | next [-]

Non trailing whitespace means the string doesn't end with a space. But foo is a function that converts an AST to a string, that's totally different. Or it's a function that loops until \0 and changes all spaces to +

The spec should be a summary of what the impl is supposed to do. You'd want more than just doesn't end with whitespace of course.

▲

bluGill 29 minutes ago | parent | prev | next [-]

> In other words, if I have the full formal spec of f(), isn't that the same thing as having f()?

In some cases, however quite often, the spec is much simpler. For instance, it's easy to say that after running sort on some list, that the result is sorted. However, it is very hard to come up with the algorithm to do that from the specification. Sometimes that is even a point. Bubble sort, quick sort, tim sort, we can go on and on. There's a huge number of different sorts that computer science have discovered over the years. They all should have the same result and so you should be able to prove they do the same thing. However, in the real world there are often reasons you would prefer one to another despite all meeting the same spec.

▲

brap 10 minutes ago | parent | next [-]

This makes a lot of sense, thank you!

▲

pydry 14 minutes ago | parent | prev [-]

I did some of this stuff in college and what bugged me was that the spec actually ended up more complex than the code and it had bugs.

That was a long time ago and they said that formal methods were the future back then, too.

	▲	chadgpt3 6 minutes ago \| parent [-]
		It's possible for that to happen but probably means either the function is too trivial or you're missing some abstraction in the spec

▲

29 minutes ago | parent | prev [-]

[deleted]