3 ms·

I think you're not thinking far enough. Why not have a compiler that can take your specification and just write your program for you? You'll probably need to wr

by anon4 13y ago

I think you're not thinking far enough. Why not have a compiler that can take your specification and just write your program for you? You'll probably need to write some code yourself, which will then interface with the written-from-formal-proof code a-la quark. My intuition is that a specification that can be checked and is good enough to guarantee that your program is 100% correct should be enough to compile a full program from, possibly with some hand-written lower-level code for guidance so it doesn't fall in pathological cases like "the empty program satisfies these constraints and is easiest to generate, so here".

chriswarbo 13y ago
> Why not have a compiler that can take your specification and just write your program for you? One difficulty with this is that programs (by definition) are 'computationally relevant' whereas proofs are not. In other words, as long as we have a proof of X it doesn't make a difference which proof we happen to have. On the other hand, different functions of type X can have a big impact on a program. For starters, there are properties which are difficult to express using types. For example, we only have rudimentary ways to encode space and time usage (eg. 'cost semantics'). Without this, when we ask for a sorting algorithm we may get back bubblesort, since it's a perfectly acceptable implementation of a sorting algorithm. Also, our types will have to become incredibly precise. Rather than just encoding the properties we care about (eg. security guarantees), we need to include lots of uninteresting properties to guide the computer to what we want (compare this to guiding a genetic algorithm via a fitness function, or getting a genie to grant you a wish in exactly the way you want). At this point, you're basically writing your program in a very indirect way; you may be better off just writing one or two lines 'manually' instead of trying to steer the automated process.

by anon4 13y ago

chriswarbo 13y ago

> Why not have a compiler that can take your specification and just write your program for you? One difficulty with this is that programs (by definition) are 'computationally relevant' whereas proofs are not. In other words, as long as we have a proof of X it doesn't make a difference which proof we happen to have. On the other hand, different functions of type X can have a big impact on a program. For starters, there are properties which are difficult to express using types. For example, we only have rudimentary ways to encode space and time usage (eg. 'cost semantics'). Without this, when we ask for a sorting algorithm we may get back bubblesort, since it's a perfectly acceptable implementation of a sorting algorithm. Also, our types will have to become incredibly precise. Rather than just encoding the properties we care about (eg. security guarantees), we need to include lots of uninteresting properties to guide the computer to what we want (compare this to guiding a genetic algorithm via a fitness function, or getting a genie to grant you a wish in exactly the way you want). At this point, you're basically writing your program in a very indirect way; you may be better off just writing one or two lines 'manually' instead of trying to steer the automated process.