On Fri, Jul 11, 2014 at 3:41 PM, Matt Oliveri <[email protected]> wrote:
> No. Programmers change. They can learn a type system if it's useful. > You have always been the one aiming for some magic middle ground where > strong types for low-level programs can be used without understanding > them. I'm worried this middle ground doesn't exist. > Programmer's do change, I agree. But I have never looked for a type system that programmers did not have to understand. What I have sought is a type system that *systems* programmers will not reject out of hand. How easily those programmers will adapt is a matter of opinion. Perhaps my experience is out of date, but this is a judgment call about language design, and I'm going to stick with what I believe will be successful. On the bright side, if someone like you (or someone else) wants to design a more sophisticated language, BitC will be a useful transition. > > > To the mainstream systems programmer, the HM type system is already well > > past the line of Clarke's third law: > > > > Any sufficiently advanced technology is indistinguishable from magic. > > If that's true, it's because the mainstream systems programmer doesn't > use HM. Not knowing all the ins and outs of a system doesn't > automatically make it seem like magic. Matt, how many systems programmers do you interact with on a daily basis? Is your opinion motivated by ample experience and qualified judgment, or do you think that anybody will learn anything? Systems programmers certainly *can* learn HM-style type systems, and in some cases they have. The problem today comes in two parts: (a) the languages that use HM-style type systems are completely unsuitable to anything a systems programmer would ever want to do (and therefore are not taken seriously), and (b) setting that aside, the *benefit* of strong typing is not seen by systems programmers. In most cases they view strong typing as an impediment rather than a tool. BitC, just as it is, is an uphill battle. > > Unless we can make type-level computation feel reasonably natural to > people > > who don't know much about modern type theory, it will hinder adoption > more > > than it helps us. > > Who said anything about type level computation? Well, there was this whole discussion thread about dependent type and how that wasn't the only way to do type-level computation... > Are you saying that's the thing that makes type inference hopeless? > No, I didn't say that. > David recommended something that sounded an awful lot like type level > computation recently, as a form of metaprogramming. So what would make > it so distasteful to potential users? > I don't think anybody said that it was distasteful. My concern is that it has to be natural enough to feel reasonable and workable to a user who is relatively hostile to HM-style typing. > > > This puts us up against Voltaire: > > > > Don't let the perfect be the enemy of the good. > > What put us up against Voltaire, and how did it manage that? > The user base puts us up against that. The kind of super-fancy type system you are angling for just isn't going to be acceptable to current users of C. > To the extent that types are already specs, type checking is already > proving properties of programs. Other than that, I don't know what you > think I was suggesting. If the "extensible proof checking" thread gave > you the willies, pretend it said "extensible type checking". > Extensible type checking gives me the willies too when I examine it in the light that current C users are the target for BitC. > Think of dependent type systems as potentially a microkernel for programming languages, if that analogy isn't too terrible. Dependent types are way too big to be that microkernel for this cycle of systems programmers. Jonathan
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
