On Sat, Dec 27, 2014 at 2:13 PM, Jonathan S. Shapiro <[email protected]> wrote: > On Sat, Dec 27, 2014 at 10:48 AM, Matt Oliveri <[email protected]> wrote: >> >> This is the part where I seize the opportunity to bash strict type >> systems for low-level (or even intermediate) languages, and preach the >> virtues of proof-based correctness. ;) > > > Good plan! Can you show me your approach to fully modular proof in the > presence of separate compilation? :)
Not the details, since they don't exist yet. Unless someone came up with them since I last looked. But if you're really willing to do that for BitC, all of a sudden, I will stop what I'm doing to develop them, though it would take a while to finish. The basic idea (which I'm dusting off from about 2 years ago) is something like CompCert and VST, but to extend the machine model to also deal with other aspects of the ABI, and have the compiler spec say how language types map to ABI specs. > A constraint is a hypothesis to be discharged. Whatever language you use, it > has to be possible to express the proposition that requires solving. > > One way to think about what happened in F# is that their solution to > polymorphism required them to introduce a new parametric pattern matching > construct (static member matching) which in turn introduced a requirement > for a new constraint type. Yes, I think I understand the problem. Otherwise I would've kept quiet. The point (for me) of a proof-based approach is to not compromise on what can be expressed. I'm not saying that this here problem is the one that regular type systems can't solve. Just that there are always more things like this, until the conventional type systems become more complex than a proof system, but less useful. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
