asciilifeform: but for something like a battlefield bitcoind, this kind of thing probably cannot be avoided.
asciilifeform: i can't recommend this for 'tetris' (that was a homework)
asciilifeform: well, stops hurting after your arse dilates to fit
asciilifeform: but so long as your expectations are realistic, something like what's described in earlier link (an excruciatingly-fascist subset of ada) doesn't hurt
asciilifeform: ben_vulpes: i've historically been a skeptic of 'provably' whatevers, because the required furniture, in my experience, never failed to interfere with 'fits in head' - and the promised are often overblown
asciilifeform: BingoBoingo: wanna write the first provably-correct pgp ?
asciilifeform: the first, article claims, such arrest in europe.
asciilifeform: http://www.aif.ru/society/law/1457211 << lulz. seven citizens of spain who fought for ua rebels and returned home - arrested for 'violating the neutrality of spain' and 'violation of sovereign nation'
asciilifeform: 'I was recently on a tour of Latin America, and the only regret I have was that I didn't study Latin harder in school so I could converse with those people.'
asciilifeform: mircea_popescu: le jour de gloire est arrivé ?
asciilifeform: benkay (~benkay@unaffiliated/benkay) has joined #bitcoin-assets << divorced ?
asciilifeform finds himself writing a netbsd kernel mod, has approximately same thoughts as fella who wakes up in 'dumpster' in a back alley, 'how i came to this sort of life' ?
asciilifeform: but potentially useful for netbsd diddlers.
asciilifeform: ^ or maybe not. seems like an elaborate rehash of '80s microkernel concept
asciilifeform: (e.g. contains no detail re: 'pendleton' and 'piedmont', the directorates-of-what-shall-we-do-about-pgp cited in earlier 'crown jewels' list)☟︎
asciilifeform: among the books i can picture on the shelves at the great library of 'meta-nsa' - this tome surely has its place
asciilifeform: not something i've experienced since working with steele's 'common lisp the language'
asciilifeform: it is an immediate mindfuck to be confronted with a computing-related document written this way.
asciilifeform: the 'rationale' chapter on oop system is interesting in that it cites the 'common lisp', c++, 'eiffel', 'smalltalk' standards materials, and expects that you are familiar with them and can understand a summary of differences
asciilifeform: BingoBoingo: don't expect a repl, ada is a classical compiled thing like c or fortran
asciilifeform: uirements of Class 1 flight critical software (the most critical) are to be attained, every attempt must be made to detect errors induced by a compiler. This is expensive, but unavoidable given current technology. The pragma Reviewable applies to a partition so that the compiler can generate code to match special documentation thus permitting independent review of the object code. The following specific requirements apply...'
asciilifeform: 'Due to the well-known fact that all compilers have bugs, it is the conventional wisdom of the safety critical community to avoid assuming that the generated object code is automatically correct. For instance, the approach taken in the avionics standard DO-178B is one of Design, Review and Test [DO-178B]. As far as practical, the review and test activities are undertaken at the object code level. Indeed, if the reliability req
asciilifeform: meanwhile, in the world of sane folks,
asciilifeform: if i had to guess, i'd imagine Cr cold-welds on impact with self, or something like that
