DEV Community: Alexander Chichigin

A cold shower for a cold shower

Alexander Chichigin — Thu, 11 Jan 2024 14:23:02 +0000

Background

Hillel Wayne being a firm believer in scientific empirical methods in general and in the field of Software Engineering in particular has prepared a list of
"cold showers" — papers challenging some widely held beliefs about various aspects of Software Development.

The very first "cold shower" addresses the question of Formal Verification, specifically the belief that

"Formal Verification is a great way to write software. We should prove all of our code correct."

Unfortunately, no source for the quote is given, presumably, it's a well-known and widely-held belief, though I personally know no one who would seriously believe and argue this point in this form.

As a counterargument and a "cold shower" Hillel offers "Verification Techniques", the fourth chapter of Peter Gutmann's thesis, "The Design and Verification of a Cryptographic Security Architecture". Wayne summarizes it as

Extensive literature review showing that formal methods are hard to learn, extremely expensive to apply, and often miss critical bugs.

Also, he counterbalances it with some caveats:

Written in 2000 and doesn't cover modern tools/techniques, such as TLA+ or dependent typing.

Considering that Coq Proof Assistant was released back in 1989, I wouldn't say Dependent Types were very modern even back in 2000, but yeah, a lot of development has happened during the last 20 years...

Anyway, the thesis that "extensive literature review showing that formal methods are hard to learn, extremely expensive to apply, and often miss critical bugs" was employed in a certain online discussion to support the POV that Formal Methods are useless or at least too costly to use in practice, any caveats were ignored, and the paper was referenced as the definitive proof. This prompted me to actually take a peek inside the paper, see what actual claims the author made, and what literature he analysed.

The Fourth Chapter

I've only skimmed the initial part of the chapter and started digging in from the third section which promised to describe the problems of Formal Methods.

3. Problems with Formal Verification

The first paragraph of this section gives the following literature review:

Empirical studies of the results of applying these methods, however, have had some difficulty in finding any correlation between their use and any gains in software quality [31], with no hard evidence available that the use of formal methods can deliver reliability more cost-effectively than traditional structured methods with enhanced testing [32]. Even in places where there has been a concerted push to apply formal methods, penetration has been minimal and the value of their use has been difficult to establish, especially where high quality can be achieved through other methods [33].

The citations are for the following papers:

[31] “Observation on Industrial Practice Using Formal Methods”, Susan Gerhart, Dan Craigen, and Ted Ralston, Proceedings of the 15th International Conference on Software Engineering (ICSE’93), 1993, p.24.
[32] “How Effective Are Software Engineering Methods?”, Norman Fenton, The Journal of Systems and Software, Vol.22, No.2 (August 1993), p.141.
[33] “Industrial Applications of Formal Methods to Model, Design, and Analyze Computer Systems: An International Survey”, Dan Craigen, Susan Gerhart, and Ted Ralston, Noyes Data Corporation, 1994 (originally published by NIST).

Without digging further into the referenced papers, what catches my eye is the fact they all were more than five years old by 2000 when the "Verification Techniques" came out. As far as I can tell it's a recurring theme in the chapter: it relies on heavily outdated papers, even for the time of writing, and I see no relevance for 2024 at all...

3.1. Problems with Tools and Scalability

Issues with the scalability of both large proofs themselves and the running time of a proof assistant checking these proofs are very well-known. We can say that the invention of Symbolic Model-Checking, which scaled the approach by two orders of magnitude, led to a breakthrough in Hardware Verification, and largely won the inventors the Turing Award. But what exactly Gutmann was talking about?

Attempts to use the Boyer–Moore prover in practice lead to the observation that “the amount of effort required to verify the system was very large. The tools were often very slow, difficult to use, and unable to completely process a complex specification. There were many areas where tedious hand analysis had to be used” [46]

Sounds plausible and relatable. What source does it cite?

[46] “Verification Technology and the A1 Criteria”, Terry Vickers Benzel, ACM SIGSOFT Software Engineering Notes, Vol.10, No.4 (August 1985), p.108.

Hmm... This paper was already 15 years (sic!) old by 2000... Anyway, what's a Boyer–Moore prover?

Nqthm is a theorem prover sometimes referred to as the Boyer–Moore theorem prover. It was a precursor to ACL2.

https://en.wikipedia.org/wiki/Nqthm

Wikipedia says it was a research theorem prover that later was replaced by ACL2 with the explicit aim of producing an industrial-strength prover addressing Nqthm's performance problems. So Gutmann criticises a piece of research software for being a research software not suitable for industrial applications. Interesting... Anyway, what's up with ACL2?

Wikipedia says ACL2 first appeared in 1990 but became publicly available only in 1996. This is still 4 years before 2000, and already in 1995, ACL2 was successfully employed to verify the floating point division of the AMD K5 CPU. And was pretty popular in Hardware Verification since then.

ACL2 is intended to be an "industrial strength" version of the Boyer–Moore theorem prover, NQTHM. Toward this goal, ACL2 has many features to support clean engineering of interesting mathematical and computational theories.

Industrial users of ACL2 include AMD, Arm, Centaur Technology, IBM, Intel, Oracle, and Collins Aerospace.

ACL2 Interesting applications among other things says:

Key properties of the Sun Java Virtual Machine and its bytecode verifier were verified in ACL2. Among the properties proved were that certain invariants are maintained by class loading and that the bytecode verifier ensures that execution is safe.

That happened sometime after 2000, and Gutmann couldn't possibly write about it, but I just want you to pause and appreciate the fact that you rely on some ACL2 proofs right now if you run HotSpot JVM or use services that run on it. And Oracle Labs still doing proofs about JVM in ACL2, they hired for such a position a couple of years ago.

Now back to the section, later we read

Another approach which has been suggested is to automatically verify (in the “formal proof of correctness” sense) the specification against the implementation as it is compiled [49]. This has the disadvantage that is can’t be done using any known technology.

Well, now we at least know the technologies: proof-carrying code, binary symbolic execution and abstract interpretation, concolic testing…

3.2. Formal Methods as a Swiss Army Chainsaw

This is the section where we can expect Gutmann to debunk that "formal Verification is a great way to write software. We should prove all of our code correct" statement. More than that, we now have the source for the quote:

Formal methods have in the past been touted as the ultimate cure for all security software assurance problems, a “panacea with unbounded applicability and potency” [50]

[50] “Problems, methods, and specialisation”, Michael Jackson, Software Engineering Journal, Vol.9, No.6 (November 1994), p.249.

Wait a bit. Michael Jackson is a very well-known and well-respected researcher in Software Engineering, we know him as a deep thinker very far from fads and hype, did he really say that Formal Methods are a "panacea with unbounded applicability and potency"?

Let's look into his 1994 paper:

The continuing search for panaceas, for universal materials out of which everything can be made, for universal methods to solve all problems, strongly suggests that we have not yet begun to understand the nature of our field. Object-orientation is only the most recent in a long line of proposed panaceas, all claiming unbounded applicability and potency.

WOW, turns out it's OOP a "panacea with unbounded applicability and potency", and there's no mention of Formal Methods in sight at all!

Frankly speaking, I got very disappointed at this point and stopped reading...

5. Alternative Approaches

I've also skimmed through the rest of the chapter, and this last chapter compares XP (eXtreme Programming, do you still remember it?) as the main Agile method at the time to some "waterfall-like" methodologies you never heard and don't care about like ISO 9000, CMM, and CASE, which were criticised in the earlier sections.

Again, much better known to us now SCRUM had been developed throughout the 1990s with the defining paper appearing in 1995. Still, it hadn't gained mass adoption until later in the 2000s, thus Gutmann couldn't do a literature review on it even if he wanted to. This simply illustrates how outdated this work become in the years passed, now that we have half a dozen SCRUM variants, Lean, Kanban and several others. Likewise, Formal Methods and Theorem Provers didn't stuck in the 90s or even 2000s, improving usability, automation, performance, accreting libraries and users, and lately even actively integrating with Machine Learning methods.

Conclusion

Well, Peter Gutmann wasn't the first to totally misquote a reference changing the meaning to the opposite in a desire to support his opinion. And it doesn't make him a bad researcher. I firmly believe he did a great job at his original research and presented very valuable results. I suspect doing an extensive literature review and a thorough analysis of evidence for or against Formal Methods never was his aim and priority. I guess it was something he needed for his thesis, so he collected a big pile of somewhat outdated papers supporting his outlook on Formal Verification and threaded a believable narrative through it. That's a much-much better job than most PhD students care to do!

The only problem, this doesn't count as an "extensive literature review showing that formal methods are hard to learn, extremely expensive to apply, and often miss critical bugs". It didn't support this claim even at the time of publication, and even less so now, 20 years later.

And for the folks throwing around "scientific papers that prove or disprove bold claims" — you should actually read the papers you're waiving, and check the sources these papers cite...

Advancing AlgebraicJulia

Alexander Chichigin — Tue, 27 Jun 2023 08:50:12 +0000

Cross-posted from Julia Forem

Looks like the Topos Institute got a grant from Mozilla to further develop AlgebraicJulia: https://blog.mozilla.org/en/mozilla/mieco-alegbraic-julia-brendan-fong/

AlgebraicJulia is a damn cool project. They use advanced categorical notions like cospans and what not as a basis for compositional modelling of physical-chemical-biological-epidemiological-etc. processes. But on the surface they use good 'ol "stock and flow" diagrams that are supposed to be drawn by unsuspecting scientists, possibly from different fields. That's where compositionality becomes crucial: it guarantees that combination of any two (or more) diagrams works as expected without falling apart.

I can only speculate why they decided to use Julia for this development, but my guess is to tap into rich ecosystem of Differential Equations. Which is necessary as long as "stock and flow" diagrams (as well as many other formalisms) define a system of differential equations modelling dynamics of a real-world processes.

Anyway, as long as Mozilla's MIECO program accepts and supports individual contributors, you can get paid for developing Category Theory in Julia! How crazy is that, huh? 😄

Setting Docker build context to CWD with Compose

Alexander Chichigin — Tue, 20 Apr 2021 17:36:25 +0000

The problem is rather contrived so the solution is rarely needed. But if you'll ever find yourself in this situation apparently it's easy to get out. 😃

Suppose you want to run the same docker-compose with the same Dockerfile but from several subfolders and you don't like duplication. So you fave a folder structure like this:

project
  |- subproject1
    |- the_file.txt
  |- subproject2
    |- the_file.txt
  |- Dockerfile
  |- compose.yml

Now you'd like to run docker-compose -f ../compose.yml up from each of subproject1 and subproject2 and for docker-compose to set the context for the Dockerfile to each of the folders respectively.

You do it with $PWD as follows:

version: "3.9"
services:
  assignment:
    build:
      context: $PWD
      dockerfile: ../Dockerfile
    ports:
      - "8080:8080"
    depends_on:
      - "database"
  database:
    image: "mariadb:10.5"
    restart: "always"
    environment:
      MYSQL_ROOT_PASSWORD: "secret_pass"

in the compose.yml file. For the sake of argument we pretend we need a separate service with a database in each case.

Then you write your Dockerfile as usual:

FROM node:15

# Create app directory
WORKDIR /app

RUN npm install -g http-server

# Bundle app source
COPY . .

EXPOSE 8080
CMD [ "http-server", "-p", "8080" ]

And now for the subproject1 you should have the first text file exposed over the Web interface, and for the subproject2 the second text file.

Yep, as I told you from the start this is rarely needed because you rarely have two (or more) subprojects built with exactly the same Dockerfile. In the end it turned out I myself don't need this setup. But I spent surprisingly long time figuring (Googling) out the right config, so we all have it now laid out in the case we ever need it. 😃

An IDE for Data Science

Alexander Chichigin — Sat, 17 Apr 2021 12:03:10 +0000

A little over a year ago I stated somewhat obvious hypothesis that JetBrains develops a specialized IDE for Data Science. Now it's official.

I've got a badge. Yeah...

Alexander Chichigin — Sun, 13 Dec 2020 16:28:27 +0000

I've got a badge for "successfully" participating in the Hacktoberfest this year. Yeah, go check my profile. This means two things: not only I submitted at least four PR explicitly tagged for the Hacktoberfest, I also explicitly applied for the badge here on Dev. Double shame for me. Why?

Well, pretty much everything there's to say about Hacktoberfest was already said October 1st. And I agree with almost all of it. More than that, my own participation is an example of Hacktoberfest fraud.

First and foremost, I'm not an Open Source contributor. By far the most of code I write I write for my job and it's closed and proprietary. Thus the best thing I can do for Open Source is to just change my job to writing Open Source code full time for another company that pays for it. And frankly speaking I can do that. But I don't. So my "contribution" in Hacktoberfest is a mockery from the beginning.

Continuing the same reasoning the very idea underlining Hacktoberfest — the idea that four PRs you make over four weekends makes a difference for the Open Source — is kinda joke for the people writing Open Source full-time, 40 or more hours a week every week of every month. Especially the ones making a leaving out of it. Twice so for ones struggling to make a leaving out of Open Source.

Speaking of my actual "contributions", only two of my PRs were to someone else's repository, and that were adding just two references to a sort of "awesome list" of technical books. Another four PRs were to my own repository I've made during Hacktoberfest adding four small features each with a separate PR. If that's not a fraud that's an embarrassment for sure.

And now I'm waiting for my new shiny Hacktoberfest t-shirt, while actual Open Source contributors wait for nothing and just continue writing, testing, debugging and publishing their code as they did years before and going to do the years to come...

A tiny little bit about maintaining health

Alexander Chichigin — Thu, 12 Mar 2020 12:57:26 +0000

As long as I'm a software developer working from home and thus sitting in front of a PC for most of the day and not walking too far, I'm rather interested in maintaining my health and shape. Not that I achieved staggering results at that but I still answered this question: https://dev.to/shofol/what-kind-of-physical-exercises-do-you-maintain-to-be-fit-and-healthy-4ai6 😊

Below I reproduce my answer but I might add some more to the post later on.

Bad news: to lose weight any sort of exercises is next to useless, the only thing that helps is eat less. :(

Good news: eating way less is surprisingly easier than you think! 😃

Disclaimer: health and medicine related stuff is extremely individual. I can and will tell what I do and what and how worked for me personally. It might not work or be harmful for other people depending on their individual physiology and health. Plus I'm very far from medical education and practice, you really should consult specialists and even after that proceed with extreme caution.

OK, now to fun stuff. What if I told you you can eat at least twice as little and lose weight without feeling hungry, weak or anything? 😃

At least, that was the case for me. If anything I felt better and more energetic because I stopped overeating and feel too heavy and too sleepy. I discovered that I can literally eat twice as little as usual and not feel hungry or anything.

Being frankly I felt some discomfort at first, some unclear feeling of something not being right, being unusual. But that was just mind tricks my brain played on me. The brain doesn't like changes, it doesn't like when things don't go as usual so it makes you feel like something's wrong and as if you have to make it as before. Thus I didn't have heavy feeling in my stomach and my brain was telling me it's not right and I have to eat more to get this heavy feeling back! But assessing my actual physical state I found time and again I feel no hunger, no stomach ache, no weakness or anything. Quite contrary my actual physical state was better than usual after lunch. So I kept ignoring the signals my brain was sending and after some time I got used to eating less and it became my new norm.

Even before that I read a long post on research regarding health benefits of intermittent fasting (which are surprisingly many and proven for mice; for humans it less clear due to challenges in conducting direct experiments). So after I discovered it's so easy to eat that much less, I thought how hard can it be not to eat for a 24 hours? Apparently, again, much easier than one might think! 😃

A hint: to fast for 24 hours you need to skip just 2 meals in a row, not 3. ;) Consider this: say, you had a breakfast at 8 am. Now you skip lunch and dinner this day, sleep at night and by 8 am next morning 24 hours have passed at which point you can eat again. But I don't eat breakfast, so I just additionally skip lunch every other day or every two days, I'm not super strict about my diet. :)

Yet another piece of a diet I'm not strict about but still keep in mind and try to aim for is a Keto diet. Again you can read a lot about how it's beneficial all over the Internet. :) But as long as I'm not strict about it I'm not in ketosis, thus I'm just on a low-carb diet in the end. Still aiming at near zero carbs intake is a much more clear goal for me. Thus I always know how much carbs I should eat: exactly zero. And all the carbs I do eat are too much and against my diet. Too bad but whatever. 😃

In the end after some months past all these adjustments to my diet I lost about 10 kg. And I wasn't overweight before that either! Thus I didn't try to lose weight, it just happened. 😃

I think these actually the most important factors that can protect you from getting diabetes, back pain, cancer or heart issues. But you asked about exercises, so I'll continue. :)

First, why exercises won't really help you loose weight. Compare the numbers. In about 2 hours on a bicycle I spend about 500 kkal. I usually ride 2 to 4 times a week. Let's take maximum: 4 times a weak, thus loosing 2000 kkal per weak additionally. Now when I do literally nothing lying on a sofa all day long I spend about 3000 kkal per 24 hours. That's at least 21000 per weak. 2000 more at best change nothing for me. Most likely, I consume all the 500 kkal I spent on a bike immediately after that 'coz I feel hungry.

Does that mean you shouldn't exercise? Absolutely not! 😃

I like riding a bike very much I think it's a great activity for so many reasons and beneficial for both physical and mental health in so many ways, I can't recommend it enough! 😃

But as long as I work from home and too lazy to go to gym and weather doesn't permit riding a bike, I exercise with a kettlebell. At home, right next to my desk. :)

As for particular exercises with a kettlebell I don't think they matter much. I do whatever I feel like doing at the moment, from simple squats to swings to pushes to whatever.

Additionally to that I do some common bodyweight exercises on the days I don't do kettlebell. Anyway I never perform heavy or very intensive training, just 30-40 minutes to stay somewhat in shape. :) Overtraining is a real thing, I'm just very far from it, but you might not be if you really serious about your training. Be careful.

I hope these simple and not strict at all advice might be helpful and will encourage your curiosity and activity towards better health. 😊

DISCLAIMER AGAIN: I'm mostly healthy person, I don't have severe preexisting conditions (though I have some chronic conditions it's almost nothing) and I haven't become much healthier. Thus what I described might only help relatively healthy person become a bit more healthier, that's it. You should always consult with health professional before experimenting on yourself!

What's wrong with computational notebooks?

Alexander Chichigin — Thu, 13 Feb 2020 11:03:43 +0000

Maybe we still don't have a definitive answer, but at least we have an observational study. The link points to a summary page that have a link to the paper. But I'll summarize the summary below. 😄

Main pain-points

After observing 5 Data Scientists at work and interviewing 15 more the authors identified 9 major pain points with computational notebooks. But I'll list only a subset:

Setup of the notebook, libraries and data sets.
Exploration and visualization.
Writing code.
Version management.
Sharing and collaboration.
Reproduction and reuse.
Production deployment.

If you're a versed Data Scientist you're probably already either giggling or facepalming. Because the list above basically enumerates all the steps in your usual workflow and we have issues with every single one of them!

I now have a question "what's right with computational notebooks?" 😄

And yet the notebooks are indispensable for Data Analysis and present huge improvement upon traditional purely code-centric development. Still we have a lot to borrow from "the old ways" in particular advanced IDE features and integration with Version Control and Continuous Integration Systems.

The paper authors say there's a huge demand for new advanced tools integrating both IDE features and Notebook features. And I have an impression JetBrains are evaluating such an opportunity and maybe even already designing or developing a Data Science tailored IDE with Notebook features and support for R language and major libraries. 😊

UPDATE. Apparently there's already an R language plugin for JetBrains IDEs that JetBrains now officially support and improve. And it indeed brings some Notebook features into a full-featured IDE experience. Yet still I think they might go for a separate Data Science-oriented IDE product.

Setting up a Swift Vapor development environment on Linux

Alexander Chichigin — Mon, 06 Jan 2020 15:38:41 +0000

... which is not Ubuntu 14.04, 16.04, 16.10, 18.04 or 18.10.

As you've certainly guessed these are officially supported ones. So if you're not happened to use one of them (I use Linux Mint 19.3) official install instructions will not work (I've tried).

Luckily enough "manual" installation works pretty much automatically and out-of-the-box anyway. :)

Install Swift

Apparently official latest Ubuntu 18.04 toolchain works on my Linux Mint 19.3 just fine. I simply downloaded the archive, extracted it and added usr/bin subdirectory to my PATH and then swift worked with no issues (so far :)).

Install Vapor CLI

As we already know we can't just install Vapor CLI (aka Vapor Toolbox) simply following official instructions. Luckily building from source works as automatic as it can. :)

Step one: clone the toolbox repository into some directory and cd there.

$ git clone https://github.com/vapor/toolbox vapor-toolbox
$ cd vapor-toolbox

Step two: just build the thing with Swift! :D (Note: I copied the command from a Dockerfile in the repo).

$ swift build -c release

After that we have a self-contained executable file vapor somewhere down the hidden .build dir we can copy anywhere on our PATH (I've copied it to my $HOME/.local/bin).

$ cp .build/release/vapor ~/.local/bin/

Now we can use it! :)

$ cd /tmp
$ vapor new Hello
$ cd Hello

And after answering 2 questions (I agreed to use Fluent and choose PostgreSQL) we have our first Vapor project.

Now we can build it!

$ vapor build
Building project..
swift build
/tmp/VaporTest/Hello: error: manifest parse error(s):
Invalid semantic version string '-beta'
error:
Failed to build.

OK, just not yet.

Apparently, the toolbox missed some template data for the Package.swift. Particularly in the line 13:

.package(url: "https://github.com/vapor/fluent--driver.git", from: "-beta")

That should be

.package(url: "https://github.com/vapor/fluent-postgres-driver.git", from: "1.0.0-beta")

At least that's what I've figured from the Github repo and that worked. :)

Run build again, wait for ages... I had no nerve and time to wait till completion, I only waited for couple hours. The process is still flawed it seems... :'D