4 ms·
I think we're more likely going to see formally verified software development frameworks...something like a "verified Rails" before we see programmers using pro
by cantankerous 13y ago
I think we're more likely going to see formally verified software development frameworks...something like a "verified Rails" before we see programmers using proof-checking in the general case. Basically it'll be the model-checking software built into a framework and a tool that will tell you if your code plays well / is safe according to the model or not.
Having programmers use proof checkers to write proofs about their own software and then prove them is still very far away, if it'll ever happen at all. One can always dream happy dreams about the Curry-Howard Isomorphism, though.
- tel 13y agoYou're thinking something like Ur/Web?
- cantankerous 13y agoOh cool! I didn't know about this. Thanks for sharing. I'm going to read into it now :).
- asdasf 13y agoUr/Web has nothing to do with formal verification does it?
- lmeyerov 13y agoUr/Web uses dependent types (Ur) to build statically checked web libraries that prevent common bugs such as malformed or stale links. The exciting part (IMO) is that the 'row types' allow encoding your database schema in the type system, so it prevents bugs common to frameworks with heavy code generation, such as the ORM in Rails or template libraries in C++. The connection to formal verification is that dependent types (depending on how you do them) let you stuff custom computations into the type checking phase. The two coolest uses of dependent types (IMO) are to verify your code and, surprisingly, synthesize boilerplate. (Btw, the guy making Ur/Web is quite important in the Coq community and Ur is one of his research vehicles for these ideas.)