No, because the government collecting sales tax isn't a party to the transaction. The fee itself needs to be in exchange for a good, but the government is giving you anything marginal in exchange for sales tax, instead it's going into accounts spent for public good.
It does all seem a bit arbitrary doesn't it? If you frame it as purchasing the privilege of purchasing a certain quantity of arbitrary goods denominated in dollars then it sure looks like a fee. But obviously that isn't what is meant.
At the end of the day shall-issue permits, hyper specialized taxes, and fees all seem to amount to the same thing. However I think you can probably construct a reasonable criteria based on whether or not the other side of the transaction is fulfilled by the government and whether or not it is legal to do the thing by default. By that logic sales taxes and car tabs would indeed be taxes while fishing and camping permits would both be fees.
I don't think formally verifying my showing that the model is correct is good enough anymore. You must prove that your implementation refines the model.
I've been building a TLA style Temporal Logic library for Verus (using LLMs). My experience so far is that LLMs are surprisingly useful at generating the mechanical proof scaffolding (when they're not occasionally trying to cheat with `assume(false)` statements), but they are not a substitute for knowing what property you actually want.
reply