Esverify: LiquidHaskell inspired verification for JavaScript
esverify.org
esverify.org
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.
"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.
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.
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.
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!