January 2008
1 post
In the future...
In the future, no one will be using test-driven development. Instead, we will be using proof-driven development. A programmer will create a specification for a program in a language like Gallina and prove its safety and correctness using a proof assistant like Coq. Once done, a compiler will transform the specification and proof into an executable program which is proven to be semantically...