695 karma · joined July 14, 2018
I'm even more excited for your project in that case. I hope I can make the time to build a prototype, right now I'm doing the same for retool, and I feel very spoiled for good choices all of a sudden when it comes to backend abstractions.
But generally I'm of the opinion that auth tightly integrated into the platform has a lot of advantages. My dream is to avoid (almost) all glue between my components, I think Firebase became successful in big part because of that.
Dashboard, realtime stuff, etc are great too. RESTful APIs I can of course get with PostgREST [0], which is insanely excellent, so the value I'm looking for is to have everything managed, from hosting/storage, to security, to all the other annoying nitty-gritty that I'm likely to get wrong.
The professionals I know generally all use a couple expensive tools from Hiltl or Festool etc over time. They can justify a new machine on a single job that pays ~8k, the time saved with the right tool is often already worth it.
And of course they are smart enough to know when they can use the "best long-lasting & cheap" tools instead of the high-end equivalents. I'm looking at you Makita PJ7000 which I bought for 150.- vs a Lamello that will be >500.- or a Festool Domino for 1k.
For those that don't know, SawStop is one of the most impressive recent techical innovations in tablesaws. It basically smashes a running blade down into an aluminium crashblock as soon as it detects something conductive touching it.
It's great to watch it work: https://youtu.be/rnlTGndRi38?t=158
Also, the list is missing at least Mafell and Fein, but they are (like Hilti and Makita) simply owned by themselves. Edit: and Lamello!
- how much of the burden of writing the proof falls on me, and how much falls to the compiler? I've seen Idris type signatures, and I didn't find them super easy to grasp.
- What are the full range of things I can express? What can't I express, even with dependent types? I come from math, so I'm used to have infinite flexibility to define what goes into my set of possible values. When I first learned Haskell I was surprised that I couldn't easily define types like "this set, modulo an equivalence relation". Or something like: "Int, but only even numbers".
- how huch more effort falls to me when structuring my code, in order to pass the properties or proofs through? I already run into this all the time in Haskell, with Maybes thay I _know_ to contain a value, or Lists that I know not to be empty. There is a real trade off between writing clear code, and wrapping/unwrapping values all the time everywhere.
Length-indexed vectors is a great example, because it is such a non-story in math, and yet for programming I have to front-load all this complexity to express something so utterly trivial. It's part infuriating, part enlightening how surprisingly tricky seemingly small things can be.
2. The files are saved on my filesystem, which would be more of a hassle to keep in sync if I used the online version.
3. It slightly lowers the friction for me to work on a diagram, which completely changes how often I instinctively reach for a tool.
I often resign myself to using it for generating the first structure, and then laying it out better in an svg editor. Of course that way I lose some of the maintainability of it.
You know, all those papers you keep downloading to "read them once you get around to it".