Are there really productive projects which rely on types as a proofing system? I've always thought it added too much complexity to the code, but I'd love to see it working well somewhere. I love the idea of correctness by design.
No too my knowledge nothing is strict about a proofing system because like I said it becomes hard to do. It could be useful for ultra safe software but for most cases the complexity isn't worth it.
But that doesn't mean it's not useful to have this capability as part of your typesystem. It just doesn't need to be fully utilized.
You don't need to program a type that proves everything correct. You can program and make sure aspects of the program are MORE correct than just plain old types. typescript is a language that does this and it is very common to find types in typescript that are more "proofy" than regular types in other languages.
Typescript does this. Above there's a type that's only a couple of lines long that proves a string reversal function reverses a string. I think even going that deep is overkill but you can define things like Objects that must contain a key of a specific string where the value is either a string or a number. And then you can create a function that dynamically specifies the value of the key in TS.
I think TS is a good example of a language that practically uses proof based types. The syntax is terrible enough that it prevents people from going overboard with it and the result is the most practical application of proof based typing that I seen. What typescript tells us that proof based typing need only be sprinkled throughout your code, it shouldn't take it all over.
> Was it worth it? Yes, it is terrible, shoddy, insecure code, but he proved out a viable business with just a few hundred dollars of investment.
This feels like less of a win for the customers though. They're paying money and exposing their data insecurely, all for a product that maybe does what it's trying to do.
> Now he's hiring a developer to shore it up.
This is going to be way harder than it sounds...
I'm all for AI as a reference or productivity/learning aid, but the results without a human in the loop quickly get horrific.
It's a win for the customers. From what he's told me, there's zero churn so far despite the hacks (including one where the hacker emailed every customer about the hack).
It's because the software is that much of an improvement over the incumbents at a fraction of the cost. Better features, more flexible, easier to use, faster, etc. Everything about it is better than the two major vendors.
The rebuild will likely end up easier, IMO, because the screens and the logic is all done. Most of it just has to be moved to strict backend and then have the APIs secured correctly.
> The rebuild will likely end up easier, IMO, because the screens and the logic is all done. Most of it just has to be moved to strict backend and then have the APIs secured correctly.
How to draw an owl…
Step 1. Draw a circle.
Step 2. Draw the rest of the owl…
>The rebuild will likely end up easier, IMO, because the screens and the logic is all done. Most of it just has to be moved to strict backend and then have the APIs secured correctly.
Atlas can finally be relieved of holding up the sky, since the 'just' in that sentence is capable of even heavier lifting.
Good thing to highlight. I'm not sure I'd bet on the game plan, but uv is an incredibly useful tool which I also wouldn't have bet on. Hopefully Simonw is right, and Astral can maintain as is.
