ときどきの雑記帖 倒行逆施編

最新ページへのリンク
目次ページへのリンク

一つ前へ 2015年7月(中旬)
一つ後へ 2015年8月(上旬)

ホームへ

2015年07月31日

■_

今年も(出るなら)そろそろだなあと思って確かめたらそうだった(12ヶ月版ね) モレスキン スター・ウォーズ 2016年版ダイアリー - ジャパン スター・ウォーズ ドットコム やはりここはべーダー卿で。 Amazon.co.jp： モレスキン 限定版 STAR WARS 2016年 手帳 ウィークリー ラージ ブラック DSW12WN3Y16: Moleskine: 文房具・オフィス用品 この商品の発売予定日は2015年8月19日です。 でも、送料込みでも .com で買った方が結構安かったりするんだよな。

Quote by Ernest Hemingway: “How did you go bankrupt?" Two ways. Gradually,...”

あら。 [ANN] Looking for new LuaJIT maintainers - luajit - FreeLists

■_

■_

Coq: The world’s best macro assembler? (PDF) つーのがありまして。 

Abstract

We describe a Coq formalization of a subset of the x86 architecture.
One emphasis of the model is brevity: using dependent types, type
classes and notation we give the x86 semantics a makeover that
counters its reputation for baroqueness. We model bits, bytes, and
memory concretely using functions that can be computed inside
Coq itself; concrete representations are mapped across to math-
ematical objects in the SSREFLECT library (naturals, and inte-
gers modulo 2n) to prove theorems. Finally, we use notation to
support conventional assembly code syntax inside Coq, including
lexically-scoped labels. Ordinary Coq definitions serve as a pow-
erful “macro” feature for everything from simple conditionals and
loops to stack-allocated local variables and procedures with param-
eters. Assembly code can be assembled within Coq, producing a
sequence of hex bytes. The assembler enjoys a correctness theo-
rem relating machine code in memory to a separation-logic formula
suitable for program verification.

で、書いたプログラム例がこう 

Definition call_cdecl3 f arg1 arg2 arg3 :=
  PUSH arg3;; PUSH arg2;; PUSH arg1;;
  CALL f;; ADD ESP, 12.

Definition main (printfSlot: DWORD) :=
  (* Argument in EBX *)
  letproc fact :=
    MOV EAX, 1;;
    MOV ECX, 1;;
    (* while ECX <= EBX *)
    while (CMP ECX, EBX) CC_LE true (
      MUL ECX;; (* Multiply EAX by ECX *)
      INC ECX
    )
  in
    LOCAL format;
    MOV EBX, 10;; callproc fact;;
    MOV EDI, printfSlot;;
    call_cdecl3 [EDI] format EBX EAX;;
    MOV EBX, 12;; callproc fact;;
    MOV EDI, printfSlot;;
    call_cdecl3 [EDI] format EBX EAX;;
    RET 0;;
    format:;;
    ds "Factorial of %d is %d";; db #10;; db #0.
Compute bytesToHex
(assemble #x"C0000004" (main #x"C0000000")).

パッと見た印象だけだと、昔こんな記述のできる マクロアセンブラあったよね。 という感じなんだけど、 Coq でというところにありがたみがあるんだろうなあ。

2015年07月30日

■_

おや、Haxe の本が。これか。 Amazon.co.jp： Haxeプログラミング入門 (I/O books): 尾野政樹, ディーグエンタテインメント: 本

学研のn年の科学の附録になってて、飼ったことあるわー＞ひらたいらさん ひらたいらさん - Google 検索

■_

■_

この記事。 loop optimizations in guile -- wingolog 

loop optimizations in guile -- wingolog

loop peeling

For a long time I have wanted to do "loop peeling". Loop peeling means peeling off the first iteration of a loop. If you have a source program that looks like this: 

while foo: 
  bar() 
  baz()

Loop peeling turns it into this: 

if foo: 
  bar() 
  baz() 
  while foo: 
    bar() 
    baz()
を見て、You wouldn't think that this is actually an optimization, would you? のように思ったのだけど読み進めると色々あった。

■_

例のアレの続き。 

  大きなテキストファイルをawkで処理するときにcatで投げ込むと速い理由 - ablog
  http://d.hatena.ne.jp/yohei-a/20150728/1438099752
  http://b.hatena.ne.jp/entry/d.hatena.ne.jp/yohei-a/20150728/1438099752

  Linuxカーネルのreadahead、うまく動いてないケースがあるの ...
  https://gist.github.com/kazuho/074e2c82a2c09b9255c5

■_

The Programmable Typewriter 記事の内容はさておき If you live around Seattle and haven't visited the Living Computer Museum you really ought to go. Admission is inexpensive and they let you play with all of the computers! シアトルにそんなものがいつの間に ＞ Living Computer Museum

ふむふむ。 Home - Living Computer Museum 

Home - Living Computer Museum

The Living Computer Museum collection presents the meaningful milestones in the evolution of computers and how people use them. The collection was assembled by Microsoft cofounder Paul G. Allen as a way to preserve the history that put him and Bill Gates on the path to founding the company.

どの辺りだろうと思ってぐぐる(べんりだー)。 https://www.google.co.jp/maps/@47.5825182,-122.3346043,17z?hl=ja 大体わかった。

地図で近くを見てたらまだあった宇和島屋w (レッドモンドにあった方はなくなったと前に聞いたけど、サイトによるとベルビューに移転した?) Uwajimaya

2015年07月29日

■_

そーいや、日本語で書かれた Elixir の本てまだないのだっけ?

ピタゴラ装置のタネ明かしが見られるぞ！　「ピタゴラ装置大解説スペシャル」放送決定 - ねとらぼ 録画録画。

■_

■_

めたるしゃちょ@8/14ソニマニさんはTwitterを使っています: "「今では世界のCOBOLエンジニアの半数が日本にいると言われている...」 .... / 「日本人は、犠牲を強いる技術革新の受け入れを真剣に考えないといけない」 - ケータイ Watch http://t.co/DaxEZvyraR @ktai_watchさんから" → 「日本人は、犠牲を強いる技術革新の受け入れを真剣に考えないといけない」 - ケータイ Watch で。 

「日本人は、犠牲を強いる技術革新の受け入れを真剣に考えないといけない」 - ケータイ Watch

しかし日本では、例えばメガバンクは数千人のシステムエンジニアの雇用を維持することを前提にしており、 クラウドコンピューティングにコストメリットを見いだせていない。 今では世界のCOBOLエンジニアの半数が日本にいると言われている。

「世界のCOBOLエンジニアの半数が日本にいる(と言われている)」って どこかに確認できる数字あるんだろうか。 全世界で何人くらいいて、日本はどのくらいとか。

how many cobol programmer in the world - Google 検索 うーむ……

COBOL - Wikipedia 

COBOL - Wikipedia

ガートナー発という情報によれば、メインフレームが世界1万サイト以上あって3万8千のレガシーシステムがあり、 COBOLは全プログラム約3,100億行のうちの約65%の約2,000億行あって、毎年約50億行が増えているという [1] [2] [3]。 これはFORTRANとアセンブラを合わせた資産の数十億行に比べて圧倒的に多い。また、世界の商用データの約75%、 商用トランザクションの80%以上（Google検索の200倍以上）である。COBOL開発者は85万人以上いるが、 COBOL開発者の増加より減少がずっと速いという。

日本国内では、2004-2009年のプロジェクトデータ2,417件をまとめたIPAのレポートによると、 1位のJava（25.4%）に次いでCOBOLは16.8%で2位[4]である。

coding horror の記事 COBOL: Everywhere and Nowhere

これは2001年の記事。 COBOLコンソーシアム － 21世紀も，COBOLだね こっちは2012年。 COBOLコンソーシアム － 増え続けるCOBOL資産・必要とされ続けるCOBOL技術者

2015年07月28日

■_

あぢー ○|￣|＿

あれ、会員登録なしで読めるようになってる? ソフトウェアとコトバ - 12　GOTO Letter をめぐって - IT記者会Report

■_

■_

Infographic: C/C++ facts we learned before going ahead with CLion | JetBrains CLion Blog 色々面白い Infographic なんだけど、 #10 の Windows環境で使用されてるCコンパイラーでの 1位2位とそのシェアがw

2015年07月27日

■_

本来の発売日は数日先なんだけど購入成功。 ザ・セカンド・マシン・エイジ
ザ・セカンド・マシン・エイジ 序文読んだだけでも面白そう。

といいつつこっちもまだ半分くらいなのだった。 データを正しく見るための数学的思考――数学の言葉で世界を見る
データを正しく見るための数学的思考――数学の言葉で世界を見る

■_

2015年07月26日

■_

日本人でもドキッとするかもしれない京都観光のマナー--トリップグラフィックス - CNET Japan 「ゴミ捨て」のところ、「Don't litter」使ってますね。ふむふむ。

■_

2015年07月25日

■_

アフタヌーンの最新号、フラジャイルとか 新連載のあれとか。

■_

■_

C言語パズル集：Cにまつわる興味深い問題あれこれ | プログラミング | POSTD の。 次のプログラムは”hello-out”と出力してくれるようには”見え”ません。（実行してみてください） これ、原文(C PUZZLES, Some interesting C problems)は The following program doesn't "seem" to print "hello-out". (Try executing it) で、単語ごとの対比とすれば訳文のここにダブルクォートつけるのは妥当とも思えるんだけど、 訳文見ると見え“ません”とかにしてみたくなる。

ついでだからプログラムはどういうものだったかというとこう 

C PUZZLES, Some interesting C problems

 #include <stdio.h> 
 #include <unistd.h> 
 int main() 
 { 
         while(1) 
         { 
                 fprintf(stdout,"hello-out"); 
                 fprintf(stderr,"hello-err"); 
                 sleep(1); 
         } 
         return 0; 
 } 
 
What could be the reason?

これはあれですね■■■■■■■の■■■。 で、■■■■■を■■■■とかすれば

私がsystemdを嫌う理由 | インフラ・ミドルウェア | POSTD (訳注：7/24、いただいた翻訳フィードバックを元に記事を修正いたしました。) お、これは。 でも、どう修正されたかがちょっと気になったw

2015年07月24日

■_

Amazon にやられた……(konozamaではありません)

■_

■_

ちょっと気になってるんだけど結局のところどういう理屈でこうなってるんだろう。

2015年07月23日

■_

SFまで10000光年
SFまで10000光年 買った。

実は一時期水玉さんから 1hop のところにいたのでした。 「こんなもんいかがっすかぁ」本編にも登場してる編集の方と当時同じ草の根BBSにいて、 オフ会等でも直接会ったことが何回も。 で、「こんなもんいかがっすかぁ」にサインいただけるという話になってたはずなんだけどなあ……(^^;

■_

2015年07月22日

■_

これ。 Breaking Changes in Visual C++ The gets and _getws functions have been removed. おー。

■_

2015年07月21日

■_

秋の情報処理技術者試験の受験申し込みが始まってますが、 今回は 「合格したら受験料出すよ」 をやらないみたいです某社。 さすがにそれでは効果がないと分かったのか その金すらも惜しんだのか以下略。

■_

一つ前へ 2015年7月(中旬)
一つ後へ 2015年8月(上旬)

ホームへ

リンクはご自由にどうぞ

メールの宛先はこちらkbk AT kt DOT rim DOT or DOT jp