今朝2時頃、突如大粒の雨が降ってきたと思ったら、唐突に物凄い風が吹いてきた。
後から確認すると、時速100km超の超絶豪風で雨も凄まじかった。 20分程度だったと思うが、稲光が毎秒5回くらい発生し、それでも雨がすごいのであまり周囲が明るくならないという、信じられない状況。
写真付きの英語記事が見つからないのでフランス語記事で。 www.swissinfo.ch
redditにもトピックがあった。 https://www.reddit.com/r/Switzerland/comments/oj9x3w/heavy_rain_and_wind_last_night_in_zurich/
当然ながら架線が切れて、トラムは走っていない。
冬の豪雪はまだ「スイスだしありえる」と思ったが、今日の豪風雨は明らかに異常だ。時速100km超の風って。
これによれば、 台風 - Wikipedia 100km/hは台風並みだけども、断じてそんなレベルではなかった。 日本で強いと言われる台風の数倍強かった。 多分100km/h超というのは平均だろう。瞬間最大では200km/hや300km/hを超えたかも。
以下の記事を見つけたので。
私は大学の学部でエネルギー関係を学び*1、大学院で情報系に転科した。なのでエネルギー問題については10代から常に興味を持って情報収集している。
それでも驚異的なのは、この10年のサスティナビリティへの関心の高まりと、再生可能エネルギーの普及の速さだ。(70年代、80年代にもエネルギー問題への世界的関心の高まりはあったが、いずれも経済成長への欲求にかき消された。）
記事のタイトルにもある様に、この10年で太陽光発電のコストは劇的に下がった。これは、直接的には技術革新と量産効果によるものである*2。
以下に、太陽光発電ファームの設置場所一覧を示す。低緯度地域を中心にかなり普及していることがわかる。西欧で唯一遅れているはフランスだが、これは日本と同じ理由による。
日本でも九州は太陽光だけで需要を賄うことができていた。しかし、太陽光ファームの設置場所をみると日本よりも遥かに北(高緯度)にある国でも太陽光を使っていることがわかる。
また、ヨーロッパでは風力発電も一般的だ。私が一番最初に驚いたのは、1992年頃のスペインのタリファという都市で、ここは30年以上前から風力発電だけで電力を賄っている。
ここは大西洋から絶えず風が吹き、ウインドサーフィンの国際大会も開かれるほど地理的な恩恵がある都市であるが、それにしてもすごいことをするなあと思っていた。 そして、この10年、ヨーロッパを歩くと至る所に風力発電の風車をみることができる。
https://www.researchgate.net/figure/Map-of-onshore-Wind-farms-in-Europe_fig1_328229021
こうした流れで、いまやヨーロッパでは再生可能エネルギーを使うのが一般的になっており、家庭の電力契約も再生可能エネルギーが第一候補になる。
そして、再生可能エネルギーは実際にとても安い。
私はIrelandとZurichで電力契約したが、どちらも再生可能エネルギーで契約している。これは綺麗事だけでなく実際に安いからである。
**
あるOSSプロダクト(ここではpostgres とする)の派生プロダクトのメンテナンスで、マイナーバージョンアップする際の手順を以下に備忘録として記す。
まず、git clone。
$ git clone https://github.com/XXX/postgres.git $ cd postgres
次に対象バージョンにcheckout。
$ git checkout PG_13_STABLE
さらに作業用のブランチを作成。
$ git checkout -b dev
remoteコマンドでリポジトリを登録し、fetchでデータを取り込む。
remote コマンドでは -t オプションで必要なブランチを指定する。
$ git remote add pg13 -t REL_13_STABLE https://github.com/postgres/postgres.git $ git fetch pg13
fetchが終わればremote リポジトリは不要なので、削除しておく。
$ git remote rm pg13
git cherry-pickコマンドで、必要なコミットを取り込む。
$ git cherry-pick 8493831385814c4f22b1d5b5d8a9227a2eb82712..272d82ec6febb97ab25fd7c67e9c84f4660b16ac
競合が発生すると止まるので、git statusコマンドで競合が発生したファイルを確認し、適宜修正する。
$ git status -s
修正が終わったらgit addで修正したファイルをインデックスに追加する。
$ git add xxx/xxxx/xxx.c
cherry-pick --continueコマンドでcherry-pickを継続する。
$ git cherry-pick --continue
これを繰り返して、全てのコミットを取り込む。
dev ブランチでの作業が終わったら、元ブランチに戻ってgit mergeコマンドを実行する。 ここでは全変更を一つのコミットに集約してマージする。なので--squash と --no-commitオプションを設定する。 最後にcommit する。
$ git checkout PG_13_STABLE $ git branch * PG_13_STABLE dev $ git merge --no-commit --squash dev $ git commit -m "updated to 13.3"
世界各地にある、春の訪れを祝う祭りの一つ。Zurichでは雪だるまを模した人形を燃やすらしい。
で、今年はCOVID-19の影響で、Zurich州でなく別の州であるUriからオンラインでやっている。 誰もいない山の中で藁の山が燃えるのを眺めるというのもなかなかシュールである。
因みにヨーロッパの春祭りで一番良かったのはスペイン バレンシアの火祭り。街中に人形が飾ってあって、最終日の夜にそれら全てに火がつけられ、真夜中に大花火大会で終了。とにかく凄かった。 Zurichのは直接観る機会がないのでなんとも言えないが、所詮街中を1Kmくらい練り歩くだけの小規模なもののようだ。
この記事、ちょっと、というかかなり感覚が古くね？ qiita.com
と思っていたら、炎上目的だったようで。
autotaker on Twitter: "「形式手法はなぜ流行っていないのか？」という記事を書いて炎上させたい"
autotaker on Twitter: "形式手法をこき下ろすと見せかけて最終的に出身研究室のステマに成功した"
一連の言い訳も見苦しい。
autotaker (@autotaker1984) | Twitter
故意に不正確な情報をばら撒く形でしか自分の"小さな得意分野"をアピールできないとは、エンジニアとして不誠実極まりないし、ミジメだ。
ということで。
形式手法は80年代から本格的に開発が始まっているが、最初に大規模に報道されたのは90年代のIntelの不動小数点ユニットのバグ対策に形式手法が導入された件だろう。
つまりチップレベルでの導入。それ以前は鉄道や原子力など。ついで組み込み分野、そして現在は分散システム系。 基本的に形式手法は導入にコストがかかるため、それがペイする分野から導入が進んでいるということ。 (自分の目の前の状況だけで全体を判断すると、痛い目に遭う。)
10年前までの状況はこちらを参照 :形式手法適用事例の紹介
日本での例を挙げれば、JAXAの筑波側では積極的に形式手法を使ってるし、自動車分野もトヨタのUSAでのリコール問題をきっかけに本格的に使っている。
因みにトヨタのブレーキに問題がなかったことを証明したのも形式手法(のツールSPIN)だった。 システムが安全とは何か考える 〜トヨタ急加速問題のNASA分析を題材にして
上記のように、以前は組み込み分野が主だったが、現在は分散処理系での使用が活発。AWSでは10年前から積極的に使っていたし、 AWSにおける形式手法 分散DBでは当然のように使っている。たとえば、CockroachDBの これ やPostgresProのこれなど。
もちろん、形式手法があっても完璧なプログラムができるわけではないが、そもそもそれは考え違いで、たとえば建築CADがあるからといって完璧な建造物が作れるわけではないのと同様、形式手法は人間が手に負えない処理を補助するツールであって、完璧なプログラムをつくる魔法ではない。 だから普通に作れるレベルの複雑さのプログラムに形式手法は不要で、手に負えない複雑さをもつシステムに立ち向かうためのツールである。
(というか、大上段に構えずに、使えるものはなんでも使ってみればいいじゃん。なんでこうも保守的なんだろうね? )
10年前にこれからは分散処理系でもモデル検証や形式手法が必要になると思って試したことがある。今となっては正しいモデル化かどうか疑問だが。 interdb.hatenablog.com
もともとspinは使っていたし、今でも個人的に使う。手法でありツールなんだから必要なときに使えばいい。
あまり知られていないだけで、複数の有償ソフトウエア会社が商売になるほどの市場もある。
個人的な印象だが、形式手法といってもいろいろあり、Intelのハードウエアレベルの検証のように大成功しているものもあれば、組み込みシステムのように比較的限定された機能の検証で成果がでているものもある。最近のAWSをはじめとする分散システムの検証も成功例になるだろう。
これらの成功例は、結局のところ、元々の問題(検証しようとしている事象など)自体が数学的なモデルに落とし込みやすいものだったといえると思う。回路ロジックしかり、分散システムならデッドロックやconsistencyなど数学的に定義できるものを対象としている。
一方、うまくいっていないものは、そもそも仕様を記述できていなかったり、定義自体が曖昧だったりと、まだまだ技術として適用できる段階に達していないようにみえる。
現時点では、うまくいっているものもダメなものもどちらも形式手法として一括りにされているため、ある人は形式手法は成功していると言い、別の人はダメな技術の典型にみえるのだろう。
私見だが、形式手法は主だった技術も理論も20年以上も前のものなので、本当の課題は現場のエンジニアがそれを使いこなすかどうかだと思っている。
その意味で、AWSがTLA+を使ったことはある種のブレークスルーだったと思う。数週間でマスターできると喧騒してくれたことが、形式手法を使うコストと心理的ハードルを劇的に下げた。
次の10年、適用分野がひろがっているとよいと思っている。
1月15日の大雪から６週間、数回の積雪があったがこの１週間は日中15度近くまで上がり、空も快晴で春のような陽気。昨日は春霞だった。
比較。昨秋と今冬の同じ場所での撮影。こちらでは遠くにアルプス山脈の端っこが見える。
大雪の後に積雪があり、その後大雨が降って各所の川が氾濫し、そのまた後に積雪があって、その後は急に春の陽気と、かなり変化が激しい。 昨年は暖かいだけで樹木が軒並み折れる大雪も川が氾濫する大雨もなかったので、今年が異常なんだろう。
