It's a good thing there are Coq proofs. However, I would still like to see the paper though. A paper is supposed to be more than just a syntactic theory. Typically there is some motivation included as well.
Note that it refers to his book on the "Specification" page :)
> Seems to be a pattern for them sadly, not sure why
Can you elaborate? Agreed I could (and will) attribute more explicitly on the website, but the intention is in no way to grab credit. I just posted this reply for more background on everything: https://news.ycombinator.com/item?id=42375914
English is likely not your first language and it’s fairly obvious what you mean, but the word you’re using a lot is spelled “intention”. Not at all how it sounds, stupid English.
(It’s also likely that this minor error is spawned by the use of intension, a very uncommon word, in the description of Tree Calculus.)
Ooops, thanks for catching, typo fixed. That Tree Calculus is intenSional (https://plato.stanford.edu/entries/logic-intensional/) is one of its main selling points, so that spelling must've rewired too many motor neurons.
Tipping isn't a thing in Australia. I'm not sure I'd know the first thing for the right way to tip if I visited the US.
And yet we seem to enjoy high quality food, and I believe our hospitality wages are higher in general.
( perhaps this is all anecdotal, but tipping has never seemed to make sense to someone not in the mix of it )
Tipping is a thing in Australia, but it's not the pseudo-compulsary thing it is in the US. We do pay significantly higher hospitality wages here; nobody is going to starve if you don't tip, and nobody is going to hold it against you. However if you receive excellent service, it's customary to demonstrate your thanks with a bit extra on the bill, and it will be appreciated.
