Bootstrapping a Type System (2010)
journal.stuffwithstuff.com
journal.stuffwithstuff.com
(/s)
Edit: I won't speak about the obvious, but anyone going back in my post history and concluding "Haskell Evangelism Strikeforce with an axe to grind" with a smirk is probably mistaken. There are well-designed languages whose goals may not perfectly align with mine (hello C/Elm/Clojure) and then there are some whose confusing inconsistency of design is, well ... confusing.
Problems that actually matter is such a good indicator that someone has no idea what they're talking about.
Formalization and proofing is what MATTERS. If you ain't got that, you're basically just guessing
And that's what makes Haskell evangelists intolerable. (Even if Haskell isn't your favourite language).
Go has it's place.
C has it too, especially on devices with > 32kb memory.
I adore Scheme and it's spec, it's expressiveness, and flexibility. Doesn't mean I think it's the best language for running a game engine, though it has been done.
We all have reasons we like our languages, and what they can be, and what they're good for.
But no language is the be-all, and end-all, of languages. There are always trade-offs. It just can't be helped.
Awk is amazing at dealing with small bits of information, quickly. It's a full language, that has been used to write some large programs... But it isn't as well suited to that. As a scripting language however, it's great.
Python is my go-to for prototyping. It can be a tad inconsistent, and more verbose than my tastes, and weaker typing than I'd like, but it works well enough.
Can't we all just get along?
Go people have a point. Haskell people have a point. Their points aren't as strong as c's was, back in the day, so they don't dominate in the way c did.
We don't have a clear winner right now. Different languages bring different things. We are in another exploration phase of languages.
I'm in the process of building a tiny programming language for some Arduinos, as part of a homebrew computer.
I'm making the memory space as a stack.
But how to have a variable know it's location in the stack?
Return an int! Oh, I just reinvented the typeless pointer C has.
PLT exploration is fun, exciting, and love reading about experiments like Magpie and Wren.
But... I still use C99 at work every day, and there's nothing wrong with that.
Can I assume you mean, devices with < 32kb memory? Or is there another language you would use on devices with such as small amount of memory instead of C?
Personally I would prefer C. But I can see arguments for each of the above.
100 > 32.
You're guessing either way. By formalizing and using deductive proof on those forms, you're guessing that your forms correctly model the intended behavior, which gets harder as the forms get more powerful and abstract. You can 100% guarantee the properties that follow from the forms. You can't deductively prove that your forms are the right forms, and that becomes more important--and harder to verify--as the forms get more abstract and powerful.
Which is what irritates me about static typing zealots. Static typing is useful in that it provides deductive guarantees, but it's not free and does have tradeoffs and pitfalls. Instead of requiring 100% guarantees of correctness, you can relax it and require sufficient guarantees of correctness, which will enable you to use the same mechanisms to inductively prove more useful things more easily, and allow you to use the same mechanisms to verify more assumptions and properties than is reasonably possible with formal verification. That's a tradeoff that should be considered more often than it is.
A primitive example of this is the use of unit tests to replace some of the formal proofs done by type checkers. There are undervalued advantages to writing programs that way--leaning on inductive instead of deductive guarantees of correctness.
Now, of course, nearly all systems have many properties that you don't want to enforce by the type system. Proofs are hard work, better do them only where it's easiest or really important.
Yet, most times I hear the phrase "static typing zealots", it comes from somebody that does not have experience with a good type system and is thus completely unable to weight off the work of constructing your types and the one of getting enough tests to be sure your program works.
> Formalization and proofing is what MATTERS. If you ain't got that, you're basically just guessing
This is how you become irrelevant. "Problems that actually matter" are the problems that actually matter - matter to the people who are trying to write programs. If you're trying to write proofs, then formalizing and proofing matter. More of us are trying to write programs, though.
is the latter necessarily dependent on the former?