Comment by RGamma | Hacker News Reader

Comment by RGamma | Hacker News Reader

Parent Full thread

"The good news about computers is that they do what you tell them to do. The bad news is that they do what you tell them to do."

Short of super-intelligent general AI writing programs for us yadda yadda, I believe the answer will be to adopt formal methods more widely: Bake the intended semantics of your software with regards to some formal system into the program itself and have it only be valid if you or the computer can prove that it meets that specification (and have the specification be complete and correct of course (which can be difficult when you consider what e.g. cryptographic strength or "real-time properties" actually mean); if proof is not feasible, add in checks that make it fail gracefully at least or generate tests).

Where today the "engineering mindset" is more prevalent (Look, I can do things with it! And it does them correctly I hope.), there needs to be a shift to a more mathematical view on computation (Your program is an instance of a certain calculus and claiming to fulfill a formal specification, which needs proof), if the software complexity mentioned is to be managed better (there's a whole zoo of specification techniques and low-level formal systems available, which doesn't make this any easier).

Unfortunately support for any of this is severely lacking in popular tools (yes, there's a lot going on in academia, but I don't feel this has spilled over yet): Languages lacking a formal spec and changing frequently, compilers not proven correct, programs running on buggy processors, operating systems with unclear semantics, written in (from a type-system PoV) weakly-expressive languages using meaningless types (void, ugh), black-box peripherals. In that light I'm amazed my computer does anything at all, but clearly most of the time these things don't matter.

Then again, I'm not aware of a fully-featured and usable (comparatively to today's personal computers) formally-specified (whatever this would mean here, surely there's more than one way to define an OS for instance) and proven computing system that goes from high-level language to operating system and application ecosystem to whatever machinery is used at the bottom.

Coq and co. to the rescue (see e.g. http://compcert.inria.fr/)?

>and have it only be valid if you or the computer can prove that it meets that specification (and have the specification be complete and correct of course

Hasn't this just moved all the issues with writing code over to writing the specifications?

Somewhat, yes.

A specification framework is there to help bridge the semantic gap between what you are trying to achieve in the real world and the world of bit-banging if you will. And even if you forget a part of a specification (like saying a sorting function needs to leave behind a sorted collection but forgetting to mention that the input and output collection need to contain the exact same elements or that the input collection needs to be finite for the function to terminate), you'll still have a notion of "incremental correctness". That's why I added in the part with what specifying "cryptographic strength" would mean (e.g.: strong against what exactly?). You could leave that or time-critical properties (e.g.: this function encrypts x bits in y seconds) out and retain the notion of "functional correctness" (i.e. the ciphertext always corresponds to what the definition says it should be).

When you're writing code you'll (most of the time :)) have an idea of what you're trying to achieve. Formal specification should enable you to write that down in convenient form.

Right now the way most people code is:

Is this spec actually correct and complete? Shrug...

Does this JavaScript actually implement the spec exactly? LoL!

At least being told what to fix in your code so that it actually implements your spec is a big step up over "staring at your code really hard." Good formal systems make it easy to find inconsistencies and incompleteness in your specs. Very good formal systems should make it easy to test and verify your spec against your intent.

>Hasn't this just moved all the issues with writing code over to writing the specifications?

Not all the issues, or at least not to the same extent, and it is not like they were not there before: an incomplete or missing specification does not default to being considered correct.

Perhaps the best we can hope for from more rigorous analysis is to catch more of the cases where we are being inconsistent, making unwarranted assumptions or even being contradictory. These are not just between requirements and implementation but also within the requirements.

This may not look like much of a promise, but the silver bullets have not worked.

> a fully-featured and usable (comparatively to today's personal computers) formally-specified... and proven computing system that goes from high-level language to operating system and application ecosystem to whatever machinery is used at the bottom.

The STEPS system from VPRI sounds like it checks most of those boxes. I don't think it's publicly available right now (although it was developed with NSF funding, so may eventually be).

http://www.vpri.org/pdf/tr2012001_steps.pdf

Is any part of STEPS formally specified? My understanding is that the goal of the project was to produce a system with a minimal volume of source code. Writing specifications alongside the source would make the project bigger, not smaller.

Reply on news.ycombinator.com