Hey, this is a nice view on business. Not everything is unicorns and you can get a pretty decent opportunity aiming at smaller scale businesses. A lot of businesses that go all or nothing could be far more successful by not overstretching. I think a lot of businesses are far beyond their optimal scale - just think whether there is something necessary about Uber valuing at 50b+ and burning so many money.

I am going through some Coq tutorials and getting pretty amazed at how cool it is. But I am also thinking about how does theorem proving and other formal methods apply to web services that are basically composition of calls to other services.

This is very good stuff.

This got me thinking that maybe Coq is not harder than Idris. Actually I think it is sometimes easier because Coq neatly separates proof from program when in Idris things get a bit mixed.