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)

@grainloom @drwho I suspect we'll see more program extraction from theorem provers rather than dependently-typed systems programming languages. Rust can't help you prove your unsafe modules are correct.

@freakazoid @drwho Rust can't really prove too much, since it's not dependently typed, but I've been :thounking: ....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.

@freakazoid @drwho idk, what's wrong with just giving the language a nice C FFI? Idris already has that, and Rust uses safe wrappers around unsafe FFI calls.

@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.

@freakazoid @drwho sure, but it can't prove more just because you're generating C, can it? wouldn't linear types help with the side effects?

@grainloom @drwho Not just because you're generating C, but because the C is generated from a model of the system that covers everything the programmer wants to be able to prove.

@freakazoid @drwho Well yeah, but does it have to be the main way of generating code?

@grainloom @drwho It depends on what you're trying to accomplish. If you just want more safety, then no. If you want full formal verification of security properties, then yes.

@freakazoid @drwho Idk, C with all its weird behaviours.... doesn't that just increase the amount of things one has to prove? I guess one could target some very strict subset and compile it with CompCert.... hmm.

We need simple programming languages.

I like (mainly because I don't code in and my don't give a shit about any standard) and I used to like programming languages like , or .

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.

@grainloom @freakazoid @drwho

@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 Idris also kind of forces you to really minimize your code because proving things gets harder the larger your definitions are.

@Shamar @freakazoid @drwho Can't really speak for more experienced devs and other languages though. I think Agda is similar in this regard, it not having tactics forces people to make their proofs clean and modular and reusable.

@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 the problem with passing interface implementations around is that you lose the guarantee that you always have the same implementation, which may or may not be worth it
a lot of Haskell's extensions are only there because its type system is too limiting

@Shamar @freakazoid @drwho Idris on the other hand has a few optional features and that's it, we're gonna see how many of those will remain gated behind %language pragmas in Blodwen

@Shamar @freakazoid @drwho @abs wait, what does singleton mean here? Idris and Agda (and probably others) already have implicit arguments

@Shamar @freakazoid @drwho
I was :thounking: 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 @freakazoid @drwho It's bad if you have to repeat yourself. Among other things, you risk the possibility that you have to change what you repeat, but you forget to change it in one place.

have any of you guys heard of zig? i was wondering if anyone has already tried it.
@grainloom @freakazoid @drwho

@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.

i still don't get the 'readable' part. is it 'readable' or you mean fully or partially 'understandable'.
@grainloom @drwho @Shamar

@hansbauer @Shamar @drwho @grainloom You'll have to explain it to me then before I can tell you if I'm talking about readability or understandability, since by the definition I've been using, at least as pertains to source code, they're the same.

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.

but you are assuming the reader master the language and the analogies being made through it, right?
@grainloom @drwho @Shamar

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?

Sign in to participate in the conversation

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!