3 ms·

I've been thinking about this in regards to things like Idris vs TLA+ as well. I prefer using Idris than TLA+ simply because Idris is continually with you, type

I've been thinking about this in regards to things like Idris vs TLA+ as well. I prefer using Idris than TLA+ simply because Idris is continually with you, type checking and part of the overall design. TLA+ can be used to verify a design, but then it is not really a living, breathing part of the end product. Having deduction built into the safety of the language is preferable to only verifying it externally then having it mutate under the next engineer. It is the same with self-documenting code; if the function and variables names are clear with a sensible architecture in place, then it is easier to keep everything in sync and readable even as different engineers take over; rather than having external documentation which must be sought for, possibly discarded, and therefore not used as much as it ought. One of the things I really like about Elixir is being able to put executable tests and examples inside the module documentation. If you run the tests and it fails, you know you need to update the examples in the documentation.

simiones 5y ago
As far as I understand, Idris and dependent typing in general are only useable for small systems today - the largest systems successfully proved using dependent typing are the SEL4 kernel (which is ~10k lines of C) and the CompCert C compilers (which compiles a subset of the C language, and has only a minimalistic optimizer, if I remeber correctly). And these two have been 5-10 year PhD projects.
withinboredom 5y ago
A year (or two?) ago, I was looking at TLA+ when I stumbled across Coyote[1]. I haven't used Coyote, but it looks interesting in that it's embedded in the language itself, allowing you to "prove" that the algorithm still works when you change implementation details. 1: https://microsoft.github.io/coyote/ https://microsoft.github.io/coyote/
moksly 5y ago
Documentation is also where things run, which resources they access and how and why they do it. I’m not a big fan of executable testing or self-documenting code in smaller projects. Sure you solve a lot with good naming, but it’s usually the business logic that needs to be documented. I can easily ready how a piece of Python or C# works, but I can’t easily tell why employees who only work less than 7 hours a week and are paid in advance are excluded from the function I’m looking at. But I mean more generally. We selfhost some things, have others in azure, and have a lot of different databases and projects. It’s nice to have a reference sheet of which belong to each other.

simiones 5y ago

As far as I understand, Idris and dependent typing in general are only useable for small systems today - the largest systems successfully proved using dependent typing are the SEL4 kernel (which is ~10k lines of C) and the CompCert C compilers (which compiles a subset of the C language, and has only a minimalistic optimizer, if I remeber correctly). And these two have been 5-10 year PhD projects.

withinboredom 5y ago

A year (or two?) ago, I was looking at TLA+ when I stumbled across Coyote[1]. I haven't used Coyote, but it looks interesting in that it's embedded in the language itself, allowing you to "prove" that the algorithm still works when you change implementation details. 1: https://microsoft.github.io/coyote/ https://microsoft.github.io/coyote/

moksly 5y ago

Documentation is also where things run, which resources they access and how and why they do it. I’m not a big fan of executable testing or self-documenting code in smaller projects. Sure you solve a lot with good naming, but it’s usually the business logic that needs to be documented. I can easily ready how a piece of Python or C# works, but I can’t easily tell why employees who only work less than 7 hours a week and are paid in advance are excluded from the function I’m looking at. But I mean more generally. We selfhost some things, have others in azure, and have a lot of different databases and projects. It’s nice to have a reference sheet of which belong to each other.