philix001

The spec might not even contain the level of detail necessary for that to be possible. That possibility is what makes modeling easier than implementing the spec.

Through a process of manual refinement, you can derive an implementation from the spec and check every step with the checker, but that's is more work than implementing the formal spec manually and is an most likely an overkill in practice.

People that can write proofs in Coq and Isabelle might prefer that over the TLC approach of exhaustively checking all the possible states allowed by a TLA+ spec. But writing proofs in Coq/Isabelle/Lean/HOL is a more sophisticated skill and requires even more training on the multiple theories available in these provers. The brute force approach of TLA+/TLC is more dependable as part of an engineering process. Some specs can be really hard to prove, but easy to exhaustively check.

Start looking for small opportunities to do something different and bold. Do that before you're asked to do it. Sooner or later you will get "hired" for the kind of job where you get to do the things you described here. That's how everyone else did it.

You might want to follow the Rust developments in this area: https://areweguiyet.com/

Check my own B+-Tree implementation that I did as an exercise. It's clean and well-commented. https://gist.github.com/philix/236f82183bbb27bd01033f94fe42e...

Real database systems are more sophisticated, but the most basic B+-Tree is still very interesting.

Goetz Graefe [1] published interesting surveys on B-Trees, query optimization...

The Red Book can give you many ideas [2].

Mark Callaghan has been published a lot of stuff related to LSM recently [3].

[1] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.219...

[2] http://www.redbook.io/

[3] https://smalldatum.blogspot.com/?m=1

Enough material here to scare anyone about databases

https://jepsen.io/talks

Check Regel. It's very flexible and allows you to generate code for different programming languages. It can also work with binary data. Its main application is generation of optimized network protocol scanners.

They are. I avoided introducing an explanation of Curry-Howard isomorphism because I think that would not be very intuitive to many people because the most commonly used type systems have very little power to express logical properties about the program.

I may write another article about this.

I don't think it's common for programmers to have in depth opinions about type systems. And most of the ones who do may not really know what they're talking about.

And some neovim patches are merged upstream.

async plugins? true color support? If you have a 32-bit color capable terminal you can use any colorscheme and get real RGB colors.

People are free to fork open source projects. tarruda tried to merge the async job system before forking vim. Bram has the right to deny the patches, but the most successful projects are the ones that attract good contributors and don't depend on the output of a single coder. It's easy to say "just make vim better" without really trying to understand Vim's C codebase.

vim's source code is really hard to test. Refactoring is needed to make code testable. That's true for every project that doesn't have tests yet. Another thing that makes it really hard to contribute to vim is that it supports operating systems that don't even exist anymore. I really don't feel like spinning a VM to make sure my changes don't break it on MS-DOS. I would rather send a PR that removes MS-DOS support than support that.

https://github.com/neovim/neovim/pull/635/files

"Tim Sweeney claims that Microsoft will remove Win32, destroy Steam"

http://arstechnica.com/information-technology/2016/07/now-ti...

MASM, MS-DOS... 32/64 bit? The hardest thing about learning x86 Assembly is finding a manual that deals mostly with the CPUs ans OSes we use these days.

Accounting is actually a language. It's the language of finance. You're probably confusing accounting with finance.

To add on what @aktau said: soon we will have much more robust UI tests.

The current UI tests are hard to write and based on the ASCII output [2] of the commands of the test [1]. By using the Neovim API we will be able to rewrite these tests to look more like automated Sellenium based web app tests and make more fine grained assertions.

[1] A test: https://github.com/neovim/neovim/blob/39cdb5f214bcb1e4a918f6... [2] The expected test output spec: https://github.com/neovim/neovim/blob/39cdb5f214bcb1e4a918f6...

What if they use BTC as a store of value and not a currency?

For a sufficiently big input (N) polynomial will be faster without any doubt.

There are cases where the lower bound to solve some problems (e.g. sorting) have been proved to be less than any known algorithm at the time.

If you prove that the lower bound for any NP-Complete problem is O(p) where p is a polynomial, then P=NP and you do not necessarily have the algorithm.

http://en.wikipedia.org/wiki/Upper_and_lower_bounds

The offer/demand will adjust the price of the remaining bitcoins. Think of lost bitcoins as a small donation to all bitcoin users.