What else are we getting wrong about programming languages?
danghica.blogspot.com
danghica.blogspot.com
Like tightening the bolts. This is a really interesting idea. I could also envision a utility wizard that you could run on a piece of code that could help guide you through making things more specific by asking you questions about the code. Are tools like this out there already? Like if you've defined a string and you run the utility it would ask: “Is this variable a number? Yes/No.” and then change to ensure it's a number in your source?
EDIT: Found one for you:
At one point you do have to make a decision though. If you come from a static type system, the compiler rejects programs if it can't proof their type correctness. Dynamic languages that introduce statics types typically do it the other way 'round: in case of doubt, allow the program at compile time, and possibly throw a type exception at run time.
You can try to make separate decisions in separate scopes, but then you have problems at the boundaries between such regions.
The point I'm trying to make is that gradual typing comes with its own complexity, both on the implementation side and through cognitive load for the programmer.
It doesn't have to be any harder than a language with a JIT VM. See Strongtalk and Dart.
At one point you do have to make a decision though. If you come from a static type system, the compiler rejects programs if it can't proof their type correctness. Dynamic languages that introduce statics types typically do it the other way 'round: in case of doubt, allow the program at compile time, and possibly throw a type exception at run time.
Also wrong. See Strongtalk and Dart. If you wanted to, you could make a variant of either system not compile your app without every type specified.
C/C++ interop and OS interactions are separate issues mostly orthogonal to type systems.
Teaching would probably start without using the type annotations for simplicity. Let the students get something working first with basic dynamic code. Then teach the type annotations and reasons for using them in more advanced courses.
sub add(\number1, \number2) { number1 + number2 }
If you call `add` with simple numbers it works: say add(1, 2) # 3
Other types of number too: say add(0.1, 0.2) == 0.3 # True
It works even for newbie definitions of "number": say add('0.1', '0.2') == '0.3' # True
A sufficiently determined newbie can of course break `add`: say add('foo', 'bar') == 'waldo'
The program stops with a suitable error message ("Cannot convert string to number ...").----
The student moves on to a more advanced course...
----
Type annotations are introduced:
sub add(Numeric \number1,
Numeric \number2) { number1 + number2 }
Everything still works as expected: say add(1, 2) # 3
But we get better error checking: say add('foo', 'bar') == 'waldo'
This generates a compile-time type-checking error ("Calling add(Str, Str) will never work with declared signature (Numeric \int1, Numeric \int2)").So, reason 1 for using types: get type-checking that catches errors at compile-time.
You can use native types for closer-to-the-metal speed (compact representations, no automatic overflow checking, etc.):
sub add(num64 \number1,
num64 \number2) { number1 + number2 }
`num64` corresponds to C's double float datatype representation. This sub will likely outperform the versions of `add` that do not have natively typed parameters.A third reason for explicit types is to take advantage of C interop:
use NativeCall;
sub add(int32, int32) returns int32 is native("calculator") { * }
If you've got a local C library (called "libcalculator.so" or somesuch) then this: say add(1,2)
will call the function with the symbol name `add` in that library.And so on.
This is the Perl 6 view. See "Getting beyond static vs. dynamic" http://www.jnthn.net/papers/2015-fosdem-static-dynamic.pdf
In Perl 6:
> 1. A value.
sub (\var) { say var }
> 2. A number. sub (Numeric \var) { say var }
> 3. A floating point number. sub (Num \var) { say var }
> 4. A floating point number between 0.0 and 100.0. sub (Num \var where 0.0 .. 100.0) { say var }
> 5. A floating point number between 0.0 and 100.0, and optimize for runtime performance instead of precision. sub (num \var where 0.0 .. 100.0) { say var }
> Ada and Microsoft Visual Basic incorporate some elements of this concept but didn't take it far enough.Did they take it as far as Perl 6 per the above?
Engineers love to engineer things. Why do people invent new languages? Sometimes it's a company trying to do something new, or something hard in a different language. Other times, it's someone who enjoys languages making a new language, thinking they've finally solved all the "hard problems," where "hard problems" is defined as problems they actually care about.
If you're not making a programming language, you're probably making a DSL or something on top of another programming language, so now you have the fun and quirks of two languages.
Instead, what if we had just a few programming languages, and made them more expressive? We'd avoid problems with language incompatibilities, libraries, and other general impedance mismatches.
I chalk this up to a few of factors: 1) Your syntatic sugar is probably not as sweet as you think it is. Many times, people claim something is easier to read or work with when it is merely easier for them, and different for others. This causes confusion for people who aren't used to that syntax. Please stop trying to make boring code look interesting. Boring code is the easiest to work with and fix.
2) Languages are hard, and working on a language is a lot harder than most people think. Once your "brilliant idea for a new language feature" actually gets implemented, the more it does, the more likely it is to screw something up.
To quote Scottie: "The more they overthink the plumbing, the easier it is to stop up the drain."
3) Because of #1 and #2, language development for major languages like python and C++ are slow. People hate slow, and so they'd rather build something special for themselves, or try some new language, because it's more fantastical. If this is a project for fun, go for it. But if this is for a business, people always constantly think some new tool is the silver bullet. What actually happens is you end up hunting bugs up and down your stack, lack robust programming tools, and end up keeping up with breaking changes rather than using that new margarita machine.
You also have to face the problem that, once a feature is shipped in a programming language, you can (almost) never remove it. This is why Python2->Python3 is taking so long: it's backwards-incompatible.
People also adopt new languages and then have more of the same exact problem, and more quickly.
As for Rust, the problem becomes how do you interoperate with all the other things that aren't as "innovative." Really this means that there's a lot more work that needs to be done, either to port, adopt, or rework lower levels. This is exactly what I was saying in that "languages are hard."
Also, not being a Rust programmer, what can I do in Rust that I can't do in any other programming language? In the end, languages are about getting stuff done: expressing a program.
If you're making a language that can do all those things, and I can make a library in an existing language that can do the same job, it seems the library is winning by a lot. The library is the abstraction and the API provides the semantics.
Everything can be tapped out with paperclips on the data bus in the end. What separates different languages is how easy it is to discover the program which implements certain functionality. This is sort of like the absurdity in a rational agent always knowing what is best for them: it disregards computational complexity.
I haven't programmed in Rust, but from what I've heard is that the linear logic helps guide you away from programs which would involve use-after-free or multiple-mutation errors. The parametric type system also guides you away from certain subtle type errors other languages tend to let you get away with. Potentially, having a language which limits your search away from well-known but hard-to-avoid programming errors helps you write the correct program sooner. So long as your notion of "correct" is correct.
An important tradeoff is between (1) compile-time checks which give confidence that a program implements its specification and (2) malleability in the face of a changing specification. With too many checks, it becomes hard to change the program (though with enough checks you can have some sense of what some changes break). Without enough malleability, the code rots. I'm curious how Rust is here.
With enough of a budget, you can just throw more people at fixing defects the compiler didn't check for.
Agree. But that is a composition of both language syntax/features and libraries. For example, I could write my own HTTP library in sockets in C++, or I could use cURL. I don't need a new language for that.
I think your tradeoff is actually a false dichotomy.
The compile time checks do give you confidence that the program implements what you think you implemented (not exactly the spec), but it is really how you design your code that allows malleability for changes. Obviously a good design makes it easy to change, and a bad design makes it hard to change.
Some languages that lack these things, like Go, can make it hard. But usually it is the newer languages that I find lack these features.
While some languages are more "malleable" than others, maybe with generics / templates / parametric types, I would say it is your code and how you write it, no matter what language it is in, that matters the most to your malleability.
> With enough of a budget, you can just throw more people at fixing defects the compiler didn't check for.
You still have to throw people at the code, because compilers aren't meant to find defects, they are there to build your code, and while some of your defects prevent that from happening, compiling isn't even close to correctness. Even if your compiler checked everything, it would only check what you coded, not what the spec says.
I agree with that, but I also think of a language as being syntax, libraries, and idioms together. Libraries give words, and the base language gives the ability to coin new ones. This is something Stephen Wolfram was advertising with his rebranding of Mathematica as the Wolfram Language, since while a pattern matching execution engine is useful symbolic calculations, it is nothing compared to the body of algorithms and data already curated and ready for use.
> I could use cURL
Arguably, the cURL is itself a specialized language for interacting with different file protocols, designed so that sort of task is easy. It's an embedded DSL in C.
> I think your tradeoff is actually a false dichotomy.
I didn't mean for it to be a dichotomy, just that if you have too much of one quality then you tend to have less of the other since doing both well is hard. I was thinking about how in my experience programs in languages with lots of formalities tend to ossify and become hard to change.
> but it is really how you design your code that allows malleability for changes.
That is true, and that's why I'd rather have the language make the local concerns easy and malleable so I can spend more time thinking about the global design.
> compilers aren't meant to find defects, they are there to build your code
That is one way to view a compiler, though I appreciate how hard it is to get NullPointerException-like-defects in Haskell. I also didn't actually mean "check" for defects, I meant making it so that defects can't happen due to some language feature which precludes them. Typo-like defects, not necessarily whether the program provably matches the spec. (And spec checking tends to make the language less malleable to spec changes...)
I'm sure you'd agree that it is nice we don't have to allocate addresses by hand for variables anymore, and with it dealing with the class of errors of miscoding the address of a variable, or the difficulty of updating a program when the variable positions change. (I'm much too young to have been there for this early history, but I have compiled small programs by hand for hobby projects or educational value.) Most compiled languages don't let you use a variable which has not been declared (and at least C emits a warning) --- this can be thought of as a language feature which addresses variable address defects.
Somewhat off-topic, but have you seen this? Seems interesting:
https://intelligence.org/2016/09/12/new-paper-logical-induct...
When I said the thing about complexity, I was thinking about intuitionism. For an intuitionist, the only things which can be said to be true are the things you can believe with your faculties. This is where the "intuitionists don't believe in the law of the excluded middle" comes from --- just because you can see that something can't not be true doesn't mean you see it is --- or something like that.
I wonder if this logical induction is a sort of Bayesian intuitionism, extending logical faculties with probabilistic ones.
And, random thought, I wonder if there is a Turing-complete programming language you can design where you can prove something can be written in it, but actually finding that program is not decidable. Then, while it's true anything can be written in any language, this one would be provably infeasible to do so.
There are also several more minor ones as well, but that's the biggie.
Because one of the most valuable things a language can do is remove unnecessary components to make a coherent small set of abstractions. That's incompatible with designing a language to support everyone's favorite feature.
There's what the language can do (syntax wise), what the standard library can do, and what 3rd party libraries can do.
I agree less syntax is better. The syntax is probably the hardest part, since it is the base.
A lot of standard libraries are where the meat is though, and when these are lacking, problems quickly arise. Example: C++ before the STL (yeah, dating myself here.)
If you have good syntax and good standard libraries, then you should be able to make good 3rd party libraries.
"Language features" I typically lump into the bundle of syntatic sugar. The only time this doesn't come into effect is when you simply can't accomplish the job any other way. Overall, I agree, we should have as few as possible "language features."
Python isn't really typed, which allows it to avoid those kinds of mistakes.
Having been a Haskell programmer, I would argue that the type system is beautiful and powerful, but still not powerful enough that it's a game changer. And it may never be powerful enough.
People forget that the reason we program is to make stuff for other people. Python gets used because it's accessible to the people most connected to the real world problems. The primary in my mind is that there is too much risk involved in transitioning from messy languages to cleaner ones.
Much of that isn't just in the language, but e.g. how easy it is to debug and deploy. So I look forward to things like stacktraces for ghc, and for stack to continue maturing. I look forward to more people being comfortable with the language.
That all having been said, it's just way too easy to run into the limitsof non-dependently-typed programming in Haskell. So here's another thought, what if string type inference is a dead end?
Types are tied into multiple dispatch; so the properties are defined by the functions created for it. Moreover, JITting is type-dependent; if you call a function with a type signature, it compiles it, unless it's seen that signature before.
general purpose programs in julia: https://github.com/shashi/Escher.jl https://github.com/essenciary/Genie.jl
The most underestimated cost!
edit: disclaimer: hobbyist, never did haskell professionally
When you feel like this please file issues on those libraries!
A single language can support multiple syntaxes if the AST is exposed as a first-class construct. This makes it easy to write new syntactic front-ends. Unfortunately, the only language to date that supports this idea is Lisp, which means that this incredibly powerful idea is conflated in most people's minds with lots of irritating silly parentheses. (One of the reasons for this conflation is that once you start adopting this mindset the parens become a lot less silly and irritating, but that's another story.)
I'm currently working on cryptography code, where algebraic syntax is very convenient. Here's an excerpt from some code I'm currently working on:
(define-method (point-double (ec elliptic-curve a b c q r) x y)
(bb
lambda modp(q, (3*x*x + 2*a*x + b)/(2*y))
x3 modp(q, lambda*lambda - a - 2*x)
y3 modp(q, lambda*(x-x3)-y)
(values x3 y3)))
(define-method (point-add (ec elliptic-curve a b c q r) x1 y1 x2 y2)
(if (and (= x1 x2) (= y1 y2))
(point-double ec x1 y1)
(bb
lambda modp(q, (y1-y2)/(x1-x2))
x3 modp(q, lambda*lambda-a-x1-x2)
y3 modp(q, lambda*(x1-x3)-y1)
(values x3 y3))))
Notice that it looks like Lisp (and it is Lisp) but there's infix code seamlessly embedded. Moreover, the MODP construct automatically converts everything to modular arithmetic operations, so, for example, x/y doesn't actually divide but instead expands into (* x (modular-inverse y p)). But when I code, all I have to do is copy the mathematical formulas more or less verbatim and my compiler takes care of expanding everything out into calculations that use Montgomery reduction or whatever optimizations I want to provide. This approach also has the advantage that I can test the correctness of my protocols completely independently of the correctness of my optimizations.I try to learn about the history of computer science and I try to understand where languages have come from - and one so far I haven't dabbled with any of the Lisp languages at all. If I was a JS learner curious about Lisp - what's the easiest way for me to get started with some experiments?
https://github.com/rongarret/BWFP
It's nowhere near complete but I'm working on chapter 3 now.
http://languagelog.ldc.upenn.edu/myl/ldc/llog/jmc.pdf is another great resource for being introduced to Lisp.
That being said, the idea that a programming language is a user interface and might be primarily evaluated like one, rather than a cult object to be venerated, is intriguing. If half the effort that has been put into ever-more-esoteric type theory had been put into serious long-term studies (perhaps with non-sophomore populations?) of usability, we might know rather more and might be able to design better languages. My suspicion is that very few researchers would be willing to follow UI-driven PL research wherever it leads; at best it might skewer some sacred concepts, at worst it might lead to a bunch of inconclusive statistical hints.
Far better to stick a bone through your beard and declare your chosen flavor of { functional programming, type theory, OO, logic programming, ... } the winner.
I can't find the source but Matz said that when he was in doubt about the most easy to understand way to design some Ruby syntax, he asked his little daughter to make a choice. When I look at some other languages I'm pretty sure nobody performed any kind of usability tests on them. It's a pity because there are languages stuck within the same community of users that used those languages parents and grandparents and can't break out into the mainstream.
The "production-oriented" bit is important as well; we _need_ those features to achieve our goals, the type system features aren't just there because we like type systems. And we've resisted doing so; the most classic example being higher kinded types. People have been asking for years, and they would be useful, but there's a lot of stuff that would also be useful, and we're focusing on them first. We're very wary of adding type system features just because we can.
Like most languages, we take users' experiences into account. We find that we're more productive, and so do many of our users. And where people don't, we're working on improving it.
For example, I depend on Foo v1, and would like to upgrade to Foo v2. Currently mainstream languages either use a type system to indicate the upgrade was unsuccessful (can't catch everything, and still require the user to patch things), or allow the user to muddle along, knowing things might break subtly but not enough to be "bothersome" (e.g. node ecosystem).
So one Foo upgrade is costing O(n) in refactoring cost where n = dependents of Foo. Given enough patience the Foo author could make an adaptor between v1 and v2 to reduce it to O(1) upgrade (inside Foo itself), but this is asking so much that nobody sensibly do it, except for big projects which provide great migration warnings, codemods, bridges, etc.
This, combined with, say, plaintext structural sharing/diffing between library versions (so that code size doesn't blow up if you have 5 transitive dependencies on Foo), might solve two important problems of dependency/versioning hell imo, and keep software as fresh as realistically possible.
I understand the general version of this is uncomputable, but that's my question: is there research on constraining the expressivity of an language just enough to make version upgrade of a library mostly automatable? Here's an idea: first-class support for fetching the code of a transition between v1 and v2, half-automated by the language & tools, half community-maintained & uploaded to a dedicated place. Alternatively, push as much as possible to data instead of functions, to make writing transition code (which would simply be massaging data from one form to another) much easier, like GraphQL deprecation strategies (https://facebook.github.io/graphql/#sec-Object-Field-depreca...)
Real-life example: two React.js components written under two different React versions naturally don't interoperate. You can't include one inside another. Right now you "can", but this is thanks to sheer human effort from React.js to maintain backward compatibility, so components using React 15 work with components using 14, etc. Same for Java, Windows, and others. The language doesn't help you with that at all. Semi/fully automated version transition/code generation would be a killer language feature.
I know next to nothing about academic PL research, but this tells me enough. I know that Haskell is an academic language, and it's a good language. But then Python is a good language too, and it's apparently almost anti-academic!
Anyway, the author seems to have good ideas about where programming language research should be directed. Hopefully someone can one day find a great combination of rigor and usability in a language. Until then I'm left wondering which of the 5-10 good languages that I know I should use for a new project (or whether I should learn X this time).
Maybe what we need is more automation and support around the language instead of new languages. Building automated compilation, testing, linting infrastructure could be a way to go.
Moving away from a pure text format. If you think about it, a lot of projects already do that: Android projects and Visual Studio projects often include GUI descriptions. Sure, they are XML, technically a text format, but not designed for direct redaction by a human.
It is the thing I have realized when, despite a lot of ideological reservations, I started to like Visual C#: a programming language is linked to the way it is used, to its IDE.
I wish language designers would embrace that fact, and not assume that the IDE would be a generic text editor. I think that is holding back a lot of possible designs.
Well, Python has a) an extensive runtime library (e.g. batteries included) and b) you type some text in a file and then you can run your program without dealing with any build system. I'd argue that both of these things might more important for the average programmer than some perfect but esoteric type system.
I kinda love the language C++ but I hate dealing with all the hassles surrounding it. Why is it so complicated to include a random C++ library from the internet to my project? Why do i have to redo my build system when I switch platforms? I usually use Python for 99% of my pet projects because it is just so easy to get started. I have some hopes that Rust improves the plumbing situation for low-level programming languages.
Which is also decently documented. The importance of good documentation for libraries (and other tools) cannot be over-emphasized.
Also, just as important as the standard library are third party libraries.v The advantage of using Python (or other popular languages) is that there is probably already a library for what you want.
Perhaps it's the fact that languages have always had to accommodate the hardware, rather than the other way around.
Why don't we have CPUs and memory controllers with built-in support for type safety and garbage collection etc. on the silicon yet?
> Allen: By 1960, we had a long list of amazing languages: Lisp, APL, Fortran, COBOL, Algol 60. These are higher-level than C. We have seriously regressed, since C developed. C has destroyed our ability to advance the state of the art in automatic optimization, automatic parallelization, automatic mapping of a high-level language to the machine. This is one of the reasons compilers are . . . basically not taught much anymore in the colleges and universities.
> Seibel: Surely there are still courses on building a compiler?
> Allen: Not in lots of schools. It's shocking. there are still conferences going on, and people doing good algorithms, good work, but the payoff for that is, in my opinion, quite minimal. Because languages like C totally overspecify the solution of problems. Those kinds of languages are what is destroying computer science as a study.
> Seibel: But most newer languages these days are higher-level than C. Things like Java and C# and Python and Ruby.
> Allen: But they still overspecify.
My guess is that it is left to the programmer because that was the way C did (no type safety and malloc) and the CPUs were developed to work with C. We're still stuck with that.
I beg to differ. A well-designed Lisp, with the power of homoiconity (code-as-data, real macros), immutability by default and a sane model for concurrency. Running on the most optimized virtual machines (JVM, .NET CLR, JavaScript), with the ability to use all of their existing libraries.
I'm talking about Clojure.
Have a look at core.matrix (https://github.com/mikera/core.matrix) and vectorz.clj (https://github.com/mikera/vectorz-clj) libs. They give you almost native speeds.
If you need even more performance, checkout neanderthal (https://github.com/uncomplicate/neanderthal) which has a GPU back-end.
See http://dragan.rocks/talks/EuroClojure2016/clojure-is-not-afr...
Down/up arrows move you through slides, while left/up arrows move you through sections. Normally, you'd press down-down-down until there are no more slides, and then right to cross to the next section. ESC gives you the bird's view of the structure.
Such extra-strong typing would lead to much more robust program and reduce complexity of testing
subset Foo where /foo/;
subset Bar where 0 .. 99;
subset Baz where * > rand;
my Foo \foovar = 'Some food';
my Bar \barvar = 42;
my Baz \bazvar = 0.5; # Fails typecheck half the timeSo here's my problem, maybe I am using Haskell wrong, and somebody can give a good answer (FYI - I am big fan of Haskell, but I am still much more efficient in Python).
Let's say I write a library, I annotate all the functions with types, so I give it a nice API, and then what happens.. I realize I should have used a different type for this parameter in this library. For instance, a type class instead of normal type. But boy, it's like everywhere. Or it's a third party library and I can't really change the type signatures. I just wish sometimes that I could just "forget" the types temporarily and just borrow the existing logic, and then reintroduce different types, type check, done.
To be fair, Haskell has potential solution for this type of problem - type inference. But the thing is, once you write the (expected) type signatures into your program (which is sometimes needed to actually help the type inference, and it's also useful as a documentation), they are always there, and sometimes, they obstruct.
So I guess I wish there was a tool with which I could manage type information in the program in a lot more dynamic way than I currently do. That would, IMHO, close the gap to the dynamic languages.
What about making every type into a type class, would it do the trick? But how would the concrete type be specified, then? Would the compiler pick it?
(Maybe it's obvious, but let me point out the connection of this question to lambda calculus. I can have two functions in typed lambda calculus which are different, because they have different type signatures, but their actual semantics is identical (provided they get arguments of correct type); or in other words, if we convert both into untyped lambda calculus, we get identical functions. So the question is, why cannot we somehow reuse code from the first function, why we have to define the same code twice with different type signature?)
newtype BusinessLogicThing = BLT Int
Then you use the semantic thing instead of the other thing (with no overhead). That can help in some situations.>So I guess I wish there was a tool with which I could manage type information in the program in a lot more dynamic way than I currently do.
I write a small amount of Haskell for personal projects and I always use type annotations for top-level definitions for two reasons. 1) I write them in advance because it helps me think about what I'm doing, and 2) I like that the compiler will tell me if I accidentally change the type between successive compilations. If it weren't for the first point though, I can imagine it would be nice to omit the type signatures and then have the compiler not only infer them for me but actually place them into the source code to save itself the trouble next time whilst improving my documentation. If it could do that, the logical next step would be to have another tool to strip out all the type signatures, to give you that design-time dynamic feeling whilst still being very much static at compile time. You can refactor all you want changing signatures and the compiler will put them all back in again when you're done.
Let's say you have a function in a library that has signature Int32 -> Int32. Then you realize you need to do the same thing, but for Int64. You can't reuse it by wrapping.
The above can seem silly, but problems like that are very real for Haskell strings.
I mean, from type-purity perspective, this behavior is OK. But from practical perspective (like Python's), it's a bummer. Why you shouldn't be able to reuse existing code just with different type signatures?
For that we have typeclasses.
Javascript was built for an environment that needs to do everything not to fail, just like HTML. A javascript engine will do everything to save a bad script from yielding an error. Javascript wasn't build with code correctness in mind. In that perspective, the language is a success. I personnally don't like languages that allows the developer to add a string to an integer without yielding a type error.
Typescript can help but it is still javascript underneath. And it doesn't correct the libraries you use that are written in Javascript.
Just like the underlying machine code is hidden in modern languages, types should be totally abstracted away when programming in a high level language.
> Do you want to invest your time worrying about types or actually programming?
Another order reversal: type systems allow you to focus on programming, instead of hunting around for bugs because somebody 50 levels up the call stack passed you a value that doesn't support the interface it needs to support.
This is an endless debate of course, just wanted to throw in a typed pl fan's opinion in the mix.
Except that is false. Bug prevalence is empirically orthogonal to type system.
See Xmonad
Or are you saying that Xmonad is not buggy? But then I don't understand how it relates to empirical orthogonality at all.
Programming is inherently the art of making something specific to a use. Types help that in that you limit what the code operates on, which makes the code you write simpler, because you have less ambiguity.
Without types you end up with a different sort of monstrosity - the corner cases that you get when comparing ints to strings in Javascript, for example.
However, where static languages are lacking is in supplying proof of the rules associated with these operators. In the case of equality, that would be associativity, reflexivity and transitivity.
The factors that make Python, Ruby, Javascript, etc. popular aren't nearly as amenable to formal mathematical analysis.
For example, in F# types maintain program correctness but get out of the way. They're not about obstinate bureaucracy but a way for the compiler to remind me "dude, this is not doing what you earlier specified it should do" and then I observe that yes, I've forgotten some corner case, do a small modification to the type definition and the whole damn thing works.
If types are getting in the way then the language is not very good (by my definition C++ is not very good and I mostly earn my living writing it).
When the type is right, the implementation is trivial.
Type-theoretic monstrosities point towards incomprehension of the problem.
Tackling two problems is a triviality, an engineer worries about more.
A modern language does not hide the machine code, but abstracts it.
A type cannot be abstracted, a type is the abstraction.