For some time, I've taken an interest in software engineering. With that, I mean robust software. After learning about Ada (my first project is from 2011), I haven't looked back (at C/C++, that is); Since then, I've learned a little about formal methods. So far, a few half-hearted attempts at SPARK/Ada have been the only results.

Now, I have stumbled across a project of Bob Nystrom's: He has designed a simple programming language, Lox, and is writing (and continuously publishing) a book on how to implement it. He has chosen Java and C, but quite a few folks have taken his code and re-implemented it in various languages: Alejandro Martinez (Swift), Ivan Katanic (C++), Paul Jackson (Go), Sasha Matijasic (Python).

So, why not do a SPARK port? I have some past experience with various parsers, so writing the bare code should not be that hard. Once that is done, annotations could be added and proofs done. The advantage of this project is that Bob is doing it now, chapter by chapter; I expect to follow at more or less the same pace, so if SPARKifying means I have to change something fundamental, I do not have to do that to the complete program. Instead, I can deal with problems as they crop up in the early stages.

I should add that SPARK can be used in different ways (or maybe I should say intensities). In the simplest case, only absence of runtime errors is proven. However, it is also possible to prove functional correctness at various levels: For example, one might set out to prove that a sorting subroutine actually returns a sorted list. This approach can be extended to more and more routines and eventually encompass the whole program. I do not know how far down this path I will (manage to) go, and in any case I have no idea how to prove functional correctness for a compiler.

Time will tell, I guess. Back to writing code now.

16:06 Kein Kommentar

von kirjoittaessani

Leave a Reply