I had the pleasure of taking a functional programming course taught by one of Liquid Haskell's core contributors. Since then even relatively robust type systems have always felt a bit lacking. Strict/static typing allows a compiler to provide certain guarantees that dynamically typed languages rely on manually written unit/integration tests for, and liquid types take this a step further by allowing inline narrowing of types and specification of invariants.
The emergence of technologies like this and Rust's borrow checker have me dreaming of a future where the writing tests is increasingly unnecessary, as your language requires that you specify your invariants etc up front. That combined with something like QuickCheck may make manually writing test cases a thing of the past.
There will invariably be some need for a kind of testing. Though we very rarely utilize traditional unit tests. Property-based tests are our common testing entry point.
"Model conformance" issues can go both directions. The model can diverge from the implementation. The designer's intent can also be incorrectly expressed in the model.
Some forms of testing can be useful in describing the problem domain and expectations in a more approachable/transparent way, and those tests can be used as part of an ensemble of methods to attempt to ensure the model represents the designer's intent, and that the implementation conforms to the model.
It's also extremely unlikely that even if you're able to verify your software, that every other part of the stack/system will have the same assurances, and in those cases some forms of testing can also be useful for building trust in components that you have no proof for.
Disclaimer: this set of problems is what my company works on for life-critical systems.
About 15 years ago it was good practice in JavaScript to check the function parameters to make sure the caller didn't do anything wrong, which would throw a friendly error message to the developer. But this seem to be thrown upon by new developers, they argue that it's "code clutter". This "code clutter" however solves almost all problems with the dynamic nature of JavaScript. Also type annotations and static typing do not substitute good documentation, nor does it substitute testing.
This combined with TypeScript (which seems to be on their roadmap), and property-based testing ala QuickCheck would be a serious toolkit for writing more correct JavaScript.
Yeah, they can definitely be jarring at first. But if you use them for a little while in a terminal that supports them (I use kitty[1]), the non ligature font will look jarring instead. I'm not so sure about using them for online code samples, though...
Right- I did look at them when they first came to my attention and I do like the look. If I were more of a fan of terminal customization I would probably give them a go. But it's weird to see them in code samples online.
I remember when I first was looking at them, I realised that they aren't even all consistent. I think it was the the "<=" ligature. <= can either be glossed as a left arrow or a less-than-or-equal, and at least one font decided somewhat inexplicably that it was an arrow. These fonts have no idea what the semantics are of what you're actually coding (since they're just ligatures) so insofar <= always means less-than-or-equal then you're fine, but if you find some language where it means assignment you'll need a different font!
Surprisingly, the way this was set up seems to completely break word selection in my browser. I'm sure there's a way to make this work, but the particular way they're doing it is unsatisfactory.
The problem with using symbols that fall outside of original ASCII set is that they’re hard to type.
It feels, to me, like a failure of user interface when someone has to resort to a mouse for input.
Like watching someone trying to play a piano on screen with a mouse. I’m sure it’s possible to compose that way but it looks so clumsy compared to someone fluently playing a keyboard.
EDIT: looks like most of these fonts are just being used for substitutions. I guess I’m neutral on that. Looks nice but I think I still prefer raw text version. Could be convinced either way.
These are abusing/using the facility modern fonts have to elaborate ligatures that modify the display of characters when they sit next to each other. Which is very straightforward once you know how it works but as you've learned is confusing when you haven't and are looking at these things for the first time in a code sample.
If you copy and paste these examples into a text editor, the font won't have the ligatures and you'll see the characters as you'd expect. They're not inserting weird codepoints to display the symbols; there's a literal < and = next to each other and the font renderer looks them up in a table and renders the mathematical less-than-or-equal symbol.
English script doesn't have many ligatures (ff, and fi are common ones, the bars on the ff are combined, and the dot on the i is subsumed into the bar of the f) but some languages and scripts have lots, I think Arabic does. Cursive English is all ligatures since letters join up differently depending on the letters next to them.
The emergence of technologies like this and Rust's borrow checker have me dreaming of a future where the writing tests is increasingly unnecessary, as your language requires that you specify your invariants etc up front. That combined with something like QuickCheck may make manually writing test cases a thing of the past.