Hacker News Reader

Comment by NohatCoder | Hacker News Reader

"A specification that can be implemented using formal methods". That is just source code. If the specification can completely define arbitrary programs it is necessarily Turing complete on its own, and as such prone to the same type of bugs as any other program.

View on HN

Purely from an industrial perspective, interest in formal methods tends to split two ways:

1. Verifying really nasty algorithms, the kind you see in cryptography and embedded systems and stuff where the bugs are triggered by horrific race conditions or incredibly specific malicious inputs that even experts won't think of testing

2. High level specifications of requirements and abstract machines and stuff, where the spec is like 100 lines and the implementation is 10k and you'd prefer to catch some design bugs before you're ten sprints into coding

A lot of bugs in (1) end up being memory-related, which is why you're seeing languages with borrow checking as part of the semantics (Rust). A lot of hype these days is in (2) because it's a lot cheaper and easier to learn, at the cost of having a lower power ceiling.

What is rust most commonly used for? If Somebody learned to program with it, what sorts of projects would they work on?

I think you are speaking to one of the core tensions in formal methods. The difference between a specification and an implementation can get blurry. Where formal methods get interesting is statically proving properties about the specification. Take a simple example of a sorting algorithm. The two most commonly proved properties of these algorithms are that they 1) return a permutation of the input list (no items removed or duplicated) and 2) that the output of the list follow some sort of ordering.

One way to look at things is to say the permutation and ordering property checkers are the specification and the actual sorting algorithm is the implementation.

To your point about the specifications being Turing complete, some tools will put restrictions on the specifications to make function termination highly likely. COQ for instance requires that recursive functions be "decreasing in their inputs" AKA that subsequent calls to the same function are passed fewer items or elements than the parent.

Sorting is one of the more favorable tasks for being specified this way, for much code there is no simpler way to verify the output than running the same or equivalent code again.

If your specification language is not Turing complete then there is simply stuff you cannot specify. Of course, just because it isn't Turing complete doesn't mean it isn't perfectly adequate for writing bugs.

As soon as you need to interface with arbitrary external components, you see the value in good specifications. If JPEG-2000 was just a reference implementation and not a spec, that would work fine if only one team ever had to develop a JPEG library, and every application that read or wrote JPEG files used exactly that one library.

Since that isn't the case, having something sit at a higher level of abstraction than the actual source code is quite valuable. Additionally, it allows domain experts like image scientists and physicists, who are experts in how to compress and decompress data with minimal quality loss but may not be experts in any particular programming language, to still contribute to the spec.

I understand your last point, but my question is:

In order for domain experts to contribute to a formal specification, this specification must be, well, formal, and also serve as a very precise shared language among all domain experts and implementors (i.e. the people who are going to read the spec and build something out of it). Once you go down this road, the specification language becomes as complex as any programming language -- or maybe even more! -- and must be learned by all involved, just like any given programming language. Some people will find it easier to learn, some will struggle or find it bizarrely unfamiliar -- again, just like any given programming language. Any sufficiently expressive specification language will also be subject to the kinds of bugs and complexity that affect programming languages.

So my question is: isn't learning a shared formal specification language more or less as difficult as learning an unfamiliar programming language?

Is there a machine-readable spec for JPEGs? Did it find interesting bugs and oversights?

Reply on news.ycombinator.com