SPJ on writing a Great Grant Proposal
> Ask lots of people to help you improve your proposal. Give it to your colleagues, your friends, your spouse, your dog, and listen to what they say. If they misunderstand what you were trying to say, don’t say “you misunderstood me”; instead rewrite it so it can’t be misunderstood. If they don’t immediately see the value of what you want to achieve, rewrite it until they do.
Idle thought:
The English plural of "virus" is "viruses".
The Latin plural of "virus" would be "virūs", because it isn't second-declension, it's fourth - except that in Latin "virus" is a singulare tantum: it has no plural. "viri" is the plural of "vir", meaning "man". "Virii" is the plural of Virius, a family name.
Just so you know.
Noticed in several talks with colleagues that it's not obvious to people that you can use JSON Schema to validate TOML. Truth is, there's nothing "JSON" about JSON Schema, it validates structured objects in memory, not files. And it doesn't care or even know from where your structured object was parsed. It could be TOML, YAML, or just a hard-coded literal. Serialization format doesn't matter.
I have encountered more image descriptions on Mastodon in 24 hours than I have in Twitter in a couple of years. Seriously. I'm not exaggerating.
As a blind person, this means a lot to me. If you read this and you describe your images, thank you so, so, so much on behalf of all of us. If you don't, now you know you'll be helping random Internet strangers make sense of your posts by typing in a few more words than usual.
Some notes on type theory
Types are propositions/theorems in some logic that's paired with your language and values are proofs. I.e. a valid value X of type T is a proof that T is decidable and "true".
Computation is merely simplifying a proof.
Depending on a set of typing rules it is sometimes possible to produce different "correct by construction" values that wouldn't fuck you up. That's decidability.
The fancier your language is, the easier it is to present a value that's undecidable, uncomputable or otherwise FUBARd.
Propositions can be insidious when you try to convert between formal and informal intent. Consider what the stupidest value can satisfy your type while not doing any of the intended work (e.g. always returning empty list for "sort" function).
You need more fancier types to pin down exact details like "no, an empty list wouldn't fly, do the actual sorting, you ass".
Type inference is an epic win for programming. The fancier the types, the more difficult is inference.
Value inference (AKA proof search) is possible sometimes and is magic.
Those are basically the same with dependent typing. And it has its costs.
As they say, "a good type has half the value". This cuts both ways.
Extraordinary times call for extraordinary effort.
Most times are ordinary. Make an ordinary effort.
Toots as he pleases.