https://buttondown.email/hillelwayne/archive/defense-in-depth-is-actually-a-good-thing/
Another (pretty comprehensive) argument for combining both formal methods and testing (and code reviews, and everything else) from Hillel Wayne.
The only part I slightly disagree about is cohesion: I don't think all the techniques necessarily push code in different directions. Kinda obvious counterexample is static types and deductive functional verification: they both push code in the same direction, namely Functional Programming (yep, even in OO and other languages). Which perfectly aligns with Property-Based Testing. I'd argue it aligns with Unit Testing as well. And if all of your team does all of that — types, verification, PBT, etc. — they all will consider such code "natural" so your code reviews will push it in the same direction. Maybe, cohesion wouldn't be so bad with DiD after all. 😊
Another (pretty comprehensive) argument for combining both formal methods and testing (and code reviews, and everything else) from Hillel Wayne.
The only part I slightly disagree about is cohesion: I don't think all the techniques necessarily push code in different directions. Kinda obvious counterexample is static types and deductive functional verification: they both push code in the same direction, namely Functional Programming (yep, even in OO and other languages). Which perfectly aligns with Property-Based Testing. I'd argue it aligns with Unit Testing as well. And if all of your team does all of that — types, verification, PBT, etc. — they all will consider such code "natural" so your code reviews will push it in the same direction. Maybe, cohesion wouldn't be so bad with DiD after all. 😊
buttondown.email
Defense in Depth is actually a good thing
So my TLAConf talk is out and I was gonna talk about technique research but then I saw this tweet and knew I had to rant about it: If after-release testing...
https://deadlockempire.github.io/
Become The Scheduler and destroy miserably concurrent code thrown at you! For the Emperor!!! 😈
Become The Scheduler and destroy miserably concurrent code thrown at you! For the Emperor!!! 😈
deadlockempire.github.io
The Deadlock Empire
Slay dragons, learn
concurrency! Play the cunning Scheduler, exploit flawed
programs and defeat the armies of the Parallel Wizard.
concurrency! Play the cunning Scheduler, exploit flawed
programs and defeat the armies of the Parallel Wizard.
http://www.cs.nott.ac.uk/~pszit/cp.html
Введение в программирование используя Python от Thorsten Altenkirch. Выглядит любопытно, но что внутри — не смотрел. Зато обложка — огонь!
http://www.cs.nott.ac.uk/~psztxa/cpwp.jpg
Введение в программирование используя Python от Thorsten Altenkirch. Выглядит любопытно, но что внутри — не смотрел. Зато обложка — огонь!
http://www.cs.nott.ac.uk/~psztxa/cpwp.jpg
https://en.wikipedia.org/wiki/Mathematics_Made_Difficult
It was funny in 1972 but 50 years later in 2022 nLab took it to the whole new level. Probably mathematicians misunderstood what "post-irony" means.
It was funny in 1972 but 50 years later in 2022 nLab took it to the whole new level. Probably mathematicians misunderstood what "post-irony" means.
https://guzey.com/co-working/#why-co-work-in-the-first-place
Вот, оказывается, зачем нужен gather.town. Может, кому пригодится.
Вот, оказывается, зачем нужен gather.town. Может, кому пригодится.
Alexey Guzey
I no longer believe that it’s possible to achieve extremely high …
Starting March 2021, I’ve been spending the majority of my working time co-working with my friends over video in my virtual gather.town office.
The sessions are usually pre-scheduled, last 2-16 hours, and we do brief check-ins every 30 minutes.
Most people…
The sessions are usually pre-scheduled, last 2-16 hours, and we do brief check-ins every 30 minutes.
Most people…
https://haslab.github.io/formal-software-design/index.html
"Formal Software Design with Alloy 6"
Includes a short section on teaching with Alloy4Fun and primers on relational and temporal logics for the reference.
But didn't read yet.
"Formal Software Design with Alloy 6"
Includes a short section on teaching with Alloy4Fun and primers on relational and temporal logics for the reference.
But didn't read yet.
https://www.pcworld.com/article/559001/the-future-of-esports-is-microsoft-excel-and-its-on-espn.html
Not a joke. The competition indeed took place, and there's a winner.
Not a joke. The competition indeed took place, and there's a winner.
PCWorld
Top Excel experts will battle it out in an esports-like competition this weekend
The finals of the Financial Modeling World Cup (FMWC) take place this weekend, where the top Excel modelers will go head-to-head in an esports battle broadcast live by ESPN3 and YouTube.
https://roganmurley.com/2021/12/11/free-monads.html
Not even mentioning that monads are a fun game in itself! 😁
Not even mentioning that monads are a fun game in itself! 😁
Rogan Murley
Game rules with a Free Monad DSL
How and why I used a Free Monad DSL for my game GALGA.
https://www.youtube.com/watch?v=85fiogkCyLY
Fundamental Computing group of the University of Groningen пиарится и пытается объяснить "простым смертным" чем они занимаются (спойлер: формальной верификацией программ).
Fundamental Computing group of the University of Groningen пиарится и пытается объяснить "простым смертным" чем они занимаются (спойлер: формальной верификацией программ).
YouTube
Fundamental computing: Mathematics and logic for software we can all rely on.
Software has changed our world!
In the Fundamental Computing group of the University of Groningen, we
use mathematics and logic to develop software we can all rely on.
Want to know more?
Get in touch with us: www.rug.nl/fse/fc
Animation: Anne Mérat
In the Fundamental Computing group of the University of Groningen, we
use mathematics and logic to develop software we can all rely on.
Want to know more?
Get in touch with us: www.rug.nl/fse/fc
Animation: Anne Mérat
https://www.youtube.com/watch?v=FihLyzdjN_8
Looks like https://sciml.ai is not just a buzzword — lots of heavy math behind: differential equations, numerical analysis, statistics and static source code analysis.
Looks like https://sciml.ai is not just a buzzword — lots of heavy math behind: differential equations, numerical analysis, statistics and static source code analysis.
YouTube
The Use and Practice of Scientific Machine Learning (Chris Rackauckas) - nextgen_ai Freiburg 2021
Chis Rackauckas' talk on "The Use and Practice of Scientific Machine Learning"
Abstract:
Scientific machine learning (SciML) methods allow for the automatic discovery of mechanistic models by infusing neural network training into the simulation process.…
Abstract:
Scientific machine learning (SciML) methods allow for the automatic discovery of mechanistic models by infusing neural network training into the simulation process.…
https://tmandry.gitlab.io/blog/posts/2021-12-21-context-capabilities/
Funny how Rust grows closer and closer to Scala 3. 😄
Funny how Rust grows closer and closer to Scala 3. 😄
Tyler Mandry
Contexts and capabilities in Rust
I recently stumbled on a promising idea to solve what I’ll call the “context problem” in Rust. The idea takes inspiration from features in other languages like implicit arguments, effects, and object capabilities. While this is at the early stages of development…
https://www.youtube.com/watch?v=CDqc9T7BYdo
Отличное эссе, очень интересно смотреть и слушать. Местами чуть перебрали пафоса, ну да чего не сделаешь для красного словца? 😃
Отличное эссе, очень интересно смотреть и слушать. Местами чуть перебрали пафоса, ну да чего не сделаешь для красного словца? 😃
YouTube
Лиготти: наследник Лавкрафта, вдохновитель «Настоящего детектива» и король ужасов (не Стивен Кинг)
По собственным подсчетам Лиготти, у него лишь несколько тысяч преданных фанатов по всему миру, а большинство читателей насилу едва вспомнят его фамилию, хотя хорошо знают Дина Кунца и Рэмси Кэмпбелла. Лиготти никогда не стремился к популярности и не раскручивал…
https://youtu.be/lAU5hx_3xRc
A really nice lecture from Xavier Leroy giving an overview of critical software development and pretty much all of existing approaches to verification. With some entertaining examples from avionics.
And a gem from a question: "Fixing bugs is not research". I'm not sure much changed since 2016...
A really nice lecture from Xavier Leroy giving an overview of critical software development and pretty much all of existing approaches to verification. With some entertaining examples from avionics.
And a gem from a question: "Fixing bugs is not research". I'm not sure much changed since 2016...
YouTube
In search of software perfection - 2016 Milner Award lecture by Dr Xavier Leroy.
2016 Milner Award lecture by Dr Xavier Leroy, a senior research scientist at Inria where he leads the Gallium research team.
In the general public, "software" has become synonymous with "crashes" and "security holes". Yet, there exists life-critical software…
In the general public, "software" has become synonymous with "crashes" and "security holes". Yet, there exists life-critical software…
👍1