Tony advised me to make money with the software model checker I have been writing. In contrast to the typical practice to make these tools open source and free for use. Would have loved to learn more from him. He was a great teacher but also a great and sharp listener. Still remember the detour we made on the way to a bar in London, talking too much and deep about refinement relations. RiP.
I can only agree. It is great work; I met Julia in several occasions were we other academics tried to push our formal methods stuff for checking properties of the Linux kernel. Also ours worked but in a way more complicated way, very resource intense, and less effective than Julia’s work.
In the end, facts are useless. You belief what you think your social bubble, and in particular, the group you think you belong to, is thinking. And many people do not speak up. Mostly those with strong (often selfish) interests speak up, and often in a manipulative way. Having narcissist or sociopaths as leader can indeed be a bad thing. Some sort of media control is good, to protect core values, to protect the law against mass manipulation.
Having a close look at the problems to be solved should be the first step. Also, Africa is big and rather heterogeneous. AI can help but is no silver bullet.
It depends on how you define testing now: Property-based testing would test sets of behaviors. The main idea is: Formalize your goal before implementing. So specification driven development would be the thing to aim for. And at some point we might be able to model check (proof) the code that has been generated. Then we are the good old idea of code synthesis.
No, that misunderstands what a proof is. It is very easy to write a SPEC that does not specify anything useful. A proof does exactly what it is supposed to do.
No, a proof proves what it proves. It does not prove what the designer of the proof intended it to prove unless the intention and the proof align. Proving that is outside of the realm of software.
The reason why property testing isnt used that much is because it is useful at catching tests only for a specific type of code which most people arent writing.
I'm not sure that's true. In essence, property tests are a method for defining types where a language lacks natural expression. In a vacuum, nearly all code could benefit from (more advanced) types. But:
1. Tradeoffs, as always. The more advanced typing you head towards, the much more time consuming it becomes to reason about the program. There is good reason for why even the most staunch type advocates rarely push for anything more advanced than monads. A handful of assertive tests is usually good enough, while requiring significantly less effort.
2. Not just time consuming, but often beyond comprehension. Most developers just don't know how to think in terms of formal proofs. Throw a language with an advanced type system, like Coq or Idris, in from of them and they wouldn't have a clue what to do with it (even ignoring the unfamiliar syntax). And with property tests, now you're asking them to not only think in advanced types, but to also effectively define the types themselves from scratch. Despite #1, I fully expect we would still see more property testing if it weren't for this huge impediment.
>Most developers just don't know how to think in terms of formal proofs
Formal proofs are useful on the same class of bug property tests are.
And vice versa.
The issue isnt necessarily that devs cant use them, it's that the problems they have which cause most bugs do not map on to the space of "what formal proofs are good at".
Tesla is not a luxury brand, but they ask for premium prices, compared to the value (worst in ADAC statistics on repairs)
“ In 1974, a new car cost an average of 5320 euros. The average income was 13,928 euros per year, so a buyer had to work for an average of 4.6 months for a new car. 20 years later, it was already 7.4 months per new car. Until 2019, this number remained stable, but then it skyrocketed. Today, a buyer has to spend all his income from 9.6 months of employment to buy a new car. For more expensive e-cars, it is even 11.4 months. The reason is stagnant incomes, but also high profit margins of the manufacturers.” https://www.tagesschau.de/wirtschaft/verbraucher/kosten-auto...
From my personal perspective, as an employed software engineer, all cars over 50k are luxury.
The value derived and average usage of a car has increased too...
Also the financing around cars have made it smoother to buy one.
Also Electric can demand a premium because they save on gas costs.
I started using emdashes in my academic career, after my advisor pointed me to the subtle differences. And since then, I like and use emdash a lot. In Latex, it is easily produced, just keep the spacing rules in mind. The Punctuation Guide is a nice reference on it https://www.thepunctuationguide.com/
There are actually four different "dashes" in La/TeX. The hyphen (-), en-dash (--) which is used for numeric rangen like 1--2, the em-dash (---) for punctuation, and the minus sign ($-$). Knuth talks about them in the TeXbook which is good fun.
Not in ASCII. My definition of plain text is roughly "the characters I have on my keyboard". Unicode is like a superset of all possible plain texts. Useful, but I really don't like my own files containing characters I can't (easily) type. If I regularly typed in another language I would acquire a keyboard for that language. I'm not even convinced typographical symbols like various dash types even belong in Unicode at all to be honest. It seems like you have to draw a very arbitrary line somewhere.
It's not too restrictive for me. I rarely need to write foreign place names or words (I'm British). Yeah I use the £ symbol so I'm not limiting myself to ASCII, just what is on my keyboard (I have € too). I just don't really consider a file full of characters I can't type to be "plain text" just because it's UTF-8, that's all.
Wherever you learned ASCII from, it was very wrong. It probably made the common (although less common in the 21st century than in the 20th) erroneous conflation of ASCII and Latin-1, or IBM code page 437, or IBM code page 850.
reply