I'm starting to see why people like #Ada (the programming language), for decades it was probably a nice alternative for systems programming, but it has so many weird moving parts and complicated rules that I'd rather use Rust.
And hopefully in a few years systems programming with dependent types will take off...
@grainloom Ada is still, unfortunately, used for application development. In a previous life, the satellite trajectory simulator we used was written in Ada, the interpreter of which sat on top of a shim to run on top of Windows XP SP3 (oddly specific OS and patch level checks), with a 32-bit GUI sitting on top. Thing was a monstrosity.
@drwho I wonder if it's better than C because of the checks it has.... or worse because who even knows what it's doing and checking.....
@drwho I heard people doing formally verified C++ and C and I think there's a reason they chose those languages instead of Ada. (although C++ is still pretty huge)
@freakazoid @drwho Rust can't really prove too much, since it's not dependently typed, but I've been ....what if instead of doing extraction like a classical build step, the language let you do some introspectiony stuff. you could have a representation of the unsafe function and prove things on that.
@grainloom @drwho The problem with trying to create a dependently typed systems programming language is that you'd need a model of the whole system's behavior, which is a massive undertaking. The system itself would also need to be well-behaved, which they're not. Program extraction lets you focus on modeling just the properties of the system that you care about.
It would be good to have libraries to make this sort of thing easier.
@grainloom @drwho The promises your unsafe code needs to make in Rust are significantly easier than they would be in a language with a more powerful typesystem. Rust mainly cares about memory safety. Calling out to C at all limits what the compiler can prove about a program. You can annotate the code with types, but that only gets you so far because of side effects. It all depends on what you want to be able to make guarantees about.
We need simple programming languages.
But now I realized that they are trying to address a problem that shouldn't be there in the first place: software complexity.
We need simple and readable programming languages that force people to keep programs simple and short.
@Shamar @freakazoid @drwho Idk, I'd agree that Rust is getting a bit too enterprise-y, but they are much more elegant to work with. I can keep my code complexity low in Rust, while also not having to suffer from the issues of C. Plan9port/9front libc is nicer to work with, sure, but it still has quite enough issues. And there are problems where you just can't get around the complexity, eg. verifying optimized cryptographic primitives:
@Shamar @freakazoid @drwho You don't really need to prove everything though, it's just encouraged. But safety by default is preferable for me. IMHO C has too many invisible pitfalls for beginners. Haskell is not that hard to learn imho and it's quite fast. Idris is just a small step up from that, it's even simpler in some ways, because proper dependent types means less weird type magic. At least that's the promise.
@Shamar @freakazoid @drwho
I was about this.....
1. verbosity can be decreased using implicit and auto arguments
2. the consistency provided by every type having only one implementation for a given typeclass is only a crutch in #Haskell, IMHO in #Idris you could - and indeed should - state all your assumptions about the parameters in the type
@Shamar @drwho @grainloom @hansbauer Zig looks like a better memory-unsafe language than C, but it's still memory-unsafe. Given how hard memory-safety issues can be to debug, can such a language ever really be considered readable? I think language constraints matter a lot to readability, because otherwise unless you fully understand the program (which is impossible for any non-trivial program), the reader and the programmer are both left to just trust the programmer.
@hansbauer @grainloom @drwho @Shamar IOW the one thing you can rely on when reading a program, assuming you've actually compiled it, is that the compiler accepts it. If the compiler accepts a larger set of incorrect programs, then the compiler's acceptance of a program tells you less than a compiler that accepts a smaller set of incorrect program.
@Shamar @drwho @grainloom @hansbauer Also, having a Turing-complete language available at compile time makes reading a program impossible in the general case due to the halting problem. Before you can understand what the compiled code actually *does*, you have to understand what code is actually being compiled. A Turing-complete macro language makes it very easy to make code that will hang or crash the compiler rather than being rejected with an error.
@hansbauer @grainloom @drwho @Shamar It also means the compiler can't output meaningful error messages in many cases, because many of your errors will be logic errors in the macro expansion phase. Which can mean understanding compile problems can itself require a debugger.
Though we see this with Lisp dialects and it's obviously not a killer there. But one is relying on the programmer to exercise restraint in their use of the macro system.
by reading a program, I can understand more or less the structures used to perform a task as defined by the symbols and rules of this language and its basic inner workings. if i master this language, i can say i read it correctly. but can i really say that i understand how this program will behave?
@grainloom @drwho @Shamar
@hansbauer @Shamar @drwho @grainloom Ah. When I talk about readability I'm talking more about how easy it is to make readable programs in the language. Any program can be made readable through literate programming, of course. But some languages lend themselves better to obfuscated code, while others lend themselves better to readable code.
i don't quite get what you mean with readability. for me a programming language, like the mathematical language, is a set of symbols and forms of flux structures. some are quite clear like if then else, because they are a primary thought pattern, but others ones are almost impossible to make explicit the same way.
@grainloom @freakazoid @drwho
@grainloom @drwho @Shamar I think we need to stop reading raw source code. It's not necessary to put the full burden of readability onto the writer when we have IDEs that can annotate code with types, either interactively or by spitting out annotated source code that could be printed.
Of course, at that point there's not much difference, since such an IDE can also autocomplete for you. But if it's all the same, why not have the source code be a minimal description?
Server run by the main developers of the project It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!