jnash

7 ms·

31.
by jnash 4y ago
100% agree. You can write bad code using both Monoliths and Microservices. However Microservices are inherently more complex and slower than Monoliths (because of the added encoding/decoding and network overhead).
32.
by jnash 4y ago
Nothing stops microservices from having the same problems. Plus all the extra problems you get with distributed systems (timing issues, logical dependencies etc.)
33.
The Power of Dependent Types (Tutorial)(idris2.readthedocs.io)
2 points by jnash 4y ago|0 comments
34.
by jnash 4y ago
No country (including the US) has "world dominance". However all countries have more or less influence and soft power on other countries.
35.
by jnash 4y ago
Having great end-to-end tests are awesome for this exact reason. I spend 99% of my time adding new cool features instead of fixing bugs. While people I work with spend all their time complaining and moaning about all the bugs that keeps pop
36.
by jnash 4y ago
I thought that was obvious? The easiest way to completely destroy the productivity of a team is to constantly switch tasks and never release anything. The team will quickly realize that the work they do doesn't matter and will switch t
37.
by jnash 4y ago
Nope. Eating healthy fats and protein is am absolute requirement for long term health. However you don't need to eat carbs at all. The body produces the little you need.
38.
by jnash 4y ago
There are tools and programming language that are already way ahead of what you are describing. Examples are Idris, F* (F-Star), Dafny etc. They use Dependent Types and/or Refinement Types to make it possible to prove your code correct
39.
by jnash 4y ago
Yep 100% agree. And the good news is that we are moving closer every day to having tools that make proving code correct practical. Languages like Idris, Agda, Liquid Haskell, F* (F-star), LEAN etc. are spearheading this movement. If Rust ha
40.
by jnash 4y ago
Can you elaborate a bit more on the kind of projects you have used Coq (and other tools) to prove correct? I am very much interested in moving in that direction career wise.
41.
by jnash 4y ago
Some companies are using the title "Proof Engineer" to mean Software Developers that specialize in proving code/hardware correct. I think that's a great choice.
42.
by jnash 4y ago
I highly recommend the programming language Idris and the book "Type-Driven Development with Idris" if you want a more "practical" introduction to proving code correct. It is a great read and every chapter pretty much bl
43.
by jnash 4y ago
Have you tried Idris? It is a "practical" programming language that also gives you the full power of Dependent Types to prove your code correct. There is a great book "Type-Driven Development with Idris" that really help
44.
A Crash Course in Idris 2(idris2.readthedocs.io)
2 points by jnash 4y ago|0 comments
45.
by jnash 4y ago
Sorry but that's a silly question. There is no limit to how complex you can make anything in any development environment. The less competent a developer is, the more complex the solution will be. What is hard, what takes skill, i
46.
by jnash 4y ago
The React architecture is very different from MVC.
47.
by jnash 4y ago
> I believe that everybody has the capacity to be creative I like your optimism but it isn't my experience. Creative people can't help but be creative. They need no prompting, no encouragement, no practice etc. They just do i
48.
by jnash 4y ago
Most of the code is open source. No problem with that.
49.
by jnash 4y ago
That's why you need to prove the whole chain end to end. From spec to C code. Hand-translating a proof to working C code will most likely introduce bugs. There are now proof tools that can prove the complete chain from spec to machine
50.
by jnash 4y ago
You are joking right? Just checking :)
51.
by jnash 4y ago
I don't think you understand what "proven correct" means. If you formally prove a spec correct using modern proof tools then it is guaranteed to have zero bugs. Nobody has found even a single bug in the proven correct CompC
52.
by jnash 4y ago
Yep if the translation is done by hand then that might be a potential problem. However a lot of modern proof tools have proven correct translators (based on the CompCert work).
53.
by jnash 4y ago
Type theory and Set theory. For example.
54.
by jnash 4y ago
> Because there's currently no high-level programming language for writing stateful software that I'm aware of. Wot? Here is how you handle state in a pure functional language like Haskell: update : Event -> State -> St
55.
by jnash 4y ago
Not my experience at all. I prefer Unity over Unreal.
56.
by jnash 4y ago
And yet C++ still rules. So I guess C++ says "Fuck You" right back.
57.
by jnash 4y ago
Unity is the #1 game engine used today. It started from nothing and bypassed Unreal. That's a very impressive feat. Also, it is so much easier to use than Unreal. So I don't see the problems you are talking about.
58.
by jnash 4y ago
You are right. The US military is primarily a jobs creation program and defense contractor beneficiary.
59.
by jnash 4y ago
Russia is not a real threat to Europe except for nuclear weapons. The defense budget of Russia is not even close to the combined defense budgets of Western Europe. Also, Europe is BIG . It would take an enormous amount of Russian soldier t
60.
Maybe Kafka Isn't Needed(thenewstack.io)
3 points by jnash 4y ago|0 comments

More ›