4 ms·

I saw the TLA+ talk [1] recently and was surprised there was no discussion of code-generation. Once you've spent a significant effort in writing and verifying

by fizixer 11y ago

I saw the TLA+ talk [1] recently and was surprised there was no discussion of code-generation. Once you've spent a significant effort in writing and verifying a formal spec for a program, there should be an automated mapping between it and the implementation, or at least a template of such implementation. [1]: https://www.youtube.com/watch?v=-4Yp3j_jk8Q https://www.youtube.com/watch?v=-4Yp3j_jk8Q

ahelwer 11y ago
There is a difference between formal specification and formal verification. Formal specification is what we have with TLA+: you create a high-level description of your system, to which you apply software tools to check the design. It's like blueprints for software. Formal verification deals with proving that the actual code you write implements a formal specification. This is a much, much harder problem. Usually, it involves cajoling a theorem prover by adding lots of annotations to your code. There's been some impressive work with the Ironclad project from MSR[1] which brought this down to ~5 lines of annotation per single line of implementation code - within striking distance of unit testing! Still, probably a decade or more away from widespread use. Formal verification isn't quite what you meant, though. You were talking about code generation. For general systems specified by TLA+, this isn't going to be useful unless you write in a very idiomatic way; in which case TLA+ is just a very high-level programming language. However, code generation is implemented in some specification languages that deal with very specific areas of system design. I'm thinking primarily of the P language[2], which is used to specify & check state machines and includes code generation capabilities for C++ and C#. [1] https://www.usenix.org/conference/osdi14/technical-sessions/presentation/hawblitzel https://www.usenix.org/conference/osdi14/technical-sessions/... [2] http://research.microsoft.com/apps/pubs/default.aspx?id=177118 http://research.microsoft.com/apps/pubs/default.aspx?id=1771...
smallape 11y ago
I can't remember which talk it was, but Lamport said for code generation you should look elsewhere.
nickpsecurity 11y ago
Code generation is a separate issue. Things you can look into are Fowler's old Perfect Developer toolkit, SCADE toolkit, model-driven development in Rockwell-Collins SHADE program, iMatix's DSL's for various things, certified compilers/optimizers for functional languages such as FLINT ML, and CompCert C compiler for low-level correspondence. Also, high-level metaprogramming systems such as Racket give you the ability to transform things in many ways. The automated programming field will have things for you. My scheme was to use a knowledge-based programming approach leveraging a combination of the above work to generate certified code from functional specifications. Haven't built it yet but would make a practical Ph.D. Hope you find some of the above enjoyable or helpful on your journey to end-to-end, verified software.

by fizixer 11y ago

ahelwer 11y ago

There is a difference between formal specification and formal verification. Formal specification is what we have with TLA+: you create a high-level description of your system, to which you apply software tools to check the design. It's like blueprints for software. Formal verification deals with proving that the actual code you write implements a formal specification. This is a much, much harder problem. Usually, it involves cajoling a theorem prover by adding lots of annotations to your code. There's been some impressive work with the Ironclad project from MSR[1] which brought this down to ~5 lines of annotation per single line of implementation code - within striking distance of unit testing! Still, probably a decade or more away from widespread use. Formal verification isn't quite what you meant, though. You were talking about code generation. For general systems specified by TLA+, this isn't going to be useful unless you write in a very idiomatic way; in which case TLA+ is just a very high-level programming language. However, code generation is implemented in some specification languages that deal with very specific areas of system design. I'm thinking primarily of the P language[2], which is used to specify & check state machines and includes code generation capabilities for C++ and C#. [1] https://www.usenix.org/conference/osdi14/technical-sessions/presentation/hawblitzel https://www.usenix.org/conference/osdi14/technical-sessions/... [2] http://research.microsoft.com/apps/pubs/default.aspx?id=177118 http://research.microsoft.com/apps/pubs/default.aspx?id=1771...

smallape 11y ago

I can't remember which talk it was, but Lamport said for code generation you should look elsewhere.

nickpsecurity 11y ago

Code generation is a separate issue. Things you can look into are Fowler's old Perfect Developer toolkit, SCADE toolkit, model-driven development in Rockwell-Collins SHADE program, iMatix's DSL's for various things, certified compilers/optimizers for functional languages such as FLINT ML, and CompCert C compiler for low-level correspondence. Also, high-level metaprogramming systems such as Racket give you the ability to transform things in many ways. The automated programming field will have things for you. My scheme was to use a knowledge-based programming approach leveraging a combination of the above work to generate certified code from functional specifications. Haven't built it yet but would make a practical Ph.D. Hope you find some of the above enjoyable or helpful on your journey to end-to-end, verified software.