Proof systems (11 Sep 2002)
- The second part of the geometric algebra series
- Perspectives Project. Maybe these people will end up with a Landscape editor.
- Self Censorship
There is a proof system for O'Caml called Coq. I keep running off to theme parks and things so I haven't had a chance to read it yet.
Some languages are "safe" in the sense that you cannot dereference NULL pointers etc. Typed languages ensure that arguments to functions cannot be of the wrong type etc. Proven languages can ensure (incomplete list):
- The program won't segfault...
- ... or buffer overflow...
- ... loop forever ...
- ... or even call API's badly
In fact you could even give everyone root permissions, but require that programs prove that they aren't doing anything wrong.
This type of thing is obviously very usefully generally but, as has been pointed out many times, we could even get rid of operating systems because no program would do anything nasty (and we could prove this). In a single-level store design having all the programs in a single address space could be a big performance boost.