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? :) 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. I actually think it's interesting that Don and I seem to have arrived independently at the need for a member matching constraint at very nearly the same time for what appear to be very different reasons. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
