Interesting languages with powerful type systems

Let's assume for a second that my waifu spent last several years worth of weekends expressing (and proving, where applicable) whatever she felt like in the type systems of Rust, Curry, Haskell, TWELF, Isabelle, HOL, Coq, SHE (https://personal.cis.strath.ac.uk/conor.mcbride/pub/she/), Epigram, Agda, Idris, and Frank (https://personal.cis.strath.ac.uk/conor.mcbride/pub/Frank/). This made her really good at formal proofs in the fields she enjoys, but now she gets bored out of her mind on weekends and at her day job. On weekends she would like to play with some more languages that are at the very least dependently-typed, can do (at least in principle, WIP languages are totally ok) equivalence reasoning, interactive type-driven program construction, automatic type->term inference (djinn, unit tests->programs), and a bit of Prolog inference in the type system. Or, alternatively, do whatever else a Programming Language Theory Freak like that could possibly enjoy. For her day job she'd wish something close to metal like Rust, but with the type system of SHE/Agda/Idris (Coq is pretty meh). Getting co-workers on board with something like that is not a problem. What would you recommend?

Check ATS and Lambda-Prolog. Instead of "language collection", you could try to learn something like Z notation, RUP, UML (modeling based software engineering) and CBSE: https://en.wikipedia.org/wiki/Z_notation https://en.wikipedia.org/wiki/Rational_Unified_Process https://en.wikipedia.org/wiki/Unified_Modeling_Language https://en.wikipedia.org/wiki/Model-driven_development https://en.wikipedia.org/wiki/Component-based_software_engineering And, maybe... do something with this knowledge? Would be good if you could develop something like a browser with formal proofs (no javascript support, please). heh >close to metal like Rust >like Rust wat?

>>598 >like Rust >wat? Well. It is closer to metal than any of the rest, except maybe some dialects of Haskell like Clean and Disciple. Rust has an attempt to have an actual memory model at the very least. > And, maybe... do something with this knowledge? She does. > Would be good if you could develop something like a browser with formal proofs (no javascript support, please). heh Sorry to inform you, but IPv4, TCP, TLS, HTTP and HTML5 standards don't have any good properties to begin with. That's not where the precious time should be spent. Plain text/markdown with links to images is good enough for almost anything. PostScript can handle the rest and has a usable subset that is simple enough to be proven formally. PostScript over Gother/9P over I2P over a sane MESH-net link layer could be good, but YouTube-addicted masses won't be interested in that.

>>599 I didn't mean to get formal proof out of protocols. What I mean was, as you pointed, a simple proof for HTML, SOCKS, HTTP GET and images decoding (jpg and png), with proper privsep. Something like links2, removing all the unneeded stuff and with formal proof. It's a project I was to run on the next years if no one does it first... Also, other idea: get into seL4 project. It really needs a POSIX layer.

>>600 I assume you expect third-party isolation, capabilities and provable zero fingerprinting for HTML privsep. For which I assume you want to track information flow between HTML layout, JS DOM and CSS selectors and block side channels properly and provably. Some of this can probably be done for some subset of HTML+JS+CSS, but PostScript subset is 1000000x easier. However, even if that gets done, in practice almost nothing would work in that subset. E.g. most of jquery won't. That's all ignoring the fact that HTML5+CSS without JS are Turing-complete already and you won't be able to termination check your layout engine. Also, how do you prove that arbitrary JS can't mount lower-abstraction layer attack on you (like ssh between tabs over CPU cache misses timing)? HTML rendering without buffer overflows, hopefully, will come with Mozilla's Servo. So, in practice, for legacy browsing I'd rather just have something like Servo without CSS media selectors on top of proved OS/VM-level sandboxing and with a Web of Trust for DAGs of JS code so that I could sign Libre JS code I read and trust and run only that to defend against theoretically undefendable soykaf. And for the new unbroken internet I want a proved PostScript engine on top of proved protocol stack. And the privsep proofs should be trivial: "simpl. simpl. there's no state. QED." All the user state should be explicit and isolated by construction. "Apps" should burn. > It's a project I was to run on the next years if no one does it first... I applaud your bravery, but I'd rather do something else. I'd rather someone would implement something like markdown+forms+pics (think BBSes, but with high-resolution pics and hyperlinks) over Gopher/9P over I2P. It could work tomorrow, be isolated in VMs the same day, have reasonably secure mostly proved and/or correct by construction toolset in a year. Personal pages, imageboards, libraries, wikis, blogs and markets would work straight away. Nothing else really matters.

>>597 >What would you recommend? If youre into type systems for proving correctness of programming errors then definately check out Ada. Ada is a language designed specifically for critical systems with no toleration for error. Just about every airliner youve ever flown in had its flight control systems coded in Ada. Ada also has an ever more strongly typed language that uses Ada syntax and is added to Ada source code as comments called SPARK. If you want strong typing in a scripting language you should check out Julia. Julia is designed to replace Matlab and R, it has very readable Python/Ruby-like syntax and is very fast. It has optional type definitions for functions and these definitions do a lot to increase the speed of JIT optimization

>>602 You're complicating things. As I said, I don't want to prove JS or CSS. The browser would be something like Links2.12, without all the bloat, and with some formal proof of correctness. No need to formal proof everything, just the critical parts. The other, non formal parts, can be just plain good code, checked with static scan (like frama-c and splint), with good privsep (pledge(2)). And this project would be meant to normal usage. I do understand that something different would be better, but if it's not compatible with the current soykaf no one will use it. I just want to browse the normal HTTP internet securely.

>>606 While Ada is very nice, and a good deal more restrictive in its type system than most mainstream imperative or OO languages, it's not really in the same league as a dependently-typed language.

In the end of the day, what gives you satisfaction is the feeling of accomplishment. Just tell her to make something quick. There is a recreational programming thread here, that might serve the purpose. >close to the metal like Rust I know some lainons talked about this before, but if she wants something really close to the metal, she should REALLY go with something close to the metal. Go make a bootloader or something, for Lain's sake. Lastly, it's not that she should ignore everything she's thought about this whole time, but she should think less about how a language is bad or not because of types. I personally hate the OOP portion of Javascript but that didn't stop me from making a small 360 panorama viewer in it for a day or two. That gave me the sense of realization and also added to my portfolio (useful if she also thinks about switching carreers, since you said she gets bored at work).

>>599 When you say "closer to the metal", do you mean that it doesn't feature a garbage collector/user is expected to provide details on whether data should be heap'd/no builtin green threading? Am I missing a detail?

I was thinking about an hypothetical language. It goes that way: - Based on Twelf - Object capability based syntax, like in E language and Pony - Dependent-type like Idris - Built-in specification constructs, like SPARK. These specifications being based on Alloy or LOTOS NT (TRAIAN, by inria) This language could be then verified at compilation time or in real-time (in a IDE) using static analysis, automated theorem proving, model checkers, specification checkers, SBSE optimization, etc. Is that even possible? Because this hypothetical language would make security errors like 99% unlikely to happen. ------ Some interesting links: - A youtube channel focused on formal verification: https://www.youtube.com/channel/UCP2eLEql4tROYmIYm5mA27A - A Cleanroom software engineering: https://en.wikipedia.org/wiki/Cleanroom_software_engineering

>>597 Can you explain what expressing/proving stuff in a type system means ? Noob here. But interested.

>>691 Well, Ada is all about writing bulletproof real-world software, not academic masturbation.

>>2352 Remember that it is that same "academic masturbation" which produces stuff like Haskell that brings to actually useful and bulletproof real-world software like Ada.

>>2363 I don't understand what you mean. Ada is way older the Haskell and not influenced by it in any way as far as I can tell.

>>2366 >> My Coq backend for ADA Spark formal verification grew on a tree. Why do you think the ML family exists?

>>2367 >Haskell influenced Ada because someone added Coq support to spark a few years ago. >I helped win World Was 2 because my uncle joined the TA for few years ago. You don't need to justify yourself because of 1 comment. Just let it go.

>>2367 >>> My Coq backend heh

>>2363 >real-world software like Ada Ada is a dead memelang for LARPers. A better example is Ocaml, Elm, and Rust.

>>2375 >Ada is a dead Just because you don't work in the industries where Ada is the only acceptable language doesn't mean no one uses it. Elm is just Javascript garbage, it might be good for making pretty web sites but obviously not used for anything important. Rust is way too new to write safety critical software with but it might get there someday. OCaml has Jane Street and ... yeah, I'm not sure how many people are actually using this language in industry. Not more than Ada I'll tell you that. If you had said F#, I might have taken you more seriously.

>>2382 I agree with you on Elm, as much as I like it for making small webpages it's at most a toy language, and its type system is so limited it guts the language. Rust is just a memelang that doesn't even have formal verification for its type system, and the code you wrote one year ago probably won't compile today despite the language reaching 1.0, I really don't understand how you could take it more seriously than OCaml, considering that OCaml has been around for decades and its core goes back even further, that MLs have been a huge inspiration for Rust and Ada, and that the Ada formal verification backend mentioned earlier was built on top of Coq, which is written in OCaml. >OCaml has Jane Street and ... yeah, I'm not sure how many people are actually using this language in industry. Bloomberg and Facebook? Unless you think that Jane Street and those other two aren't serious enough and don't run critical software. What exactly makes F# more serious than OCaml despite being almost the same language other than how the former is maintained by a serious business company? Also, please work on your reading comprehension. I mentioned Haskell in the above post not because it has influenced Ada in any way, but because the research that's being done with it will surely end up in a less academic language similar to Ada someday.

>>2384 >I really don't understand how you could take it more seriously than OCaml, considering that OCaml has been around for decades I said Rust will get there in the future. OCaml is too high level to be useful in many domains where safety is actually needed. OCaml has a garbage collector and still can't do true multithreading for example. Rust on the otherhand was designed from the start with those types of use cases in mind, that's why I think it will be more relevant to high assurance systems in the future. >What exactly makes F# more serious than OCaml That's not what I said. I said I would take *you* more seriously for mentioning F# because it is far more prevalent in real world high assurance applications (finance) than any of the other languages you mentioned. >Bloomberg and Facebook? That's not really the same thing. Facebook dicks around with things like OCaml and D for random projects but all their money making infrastructure is all PHP. Jane Street uses OCaml for their trading algorithms which is Important soykaf™ and why they came to mind first. I don't really know what Bloomberg does but ok. If you want to play that game though, a Boeing 777 flies on ~1,000,000 lines of Ada. It doesn't come much more safety critical or real world than that. >the research that's being done with it will surely end up in a less academic language similar to Ada someday. Fair enough. Keep going then.

>>2384 >Rust is just a memelang that doesn't even have formal verification for its type system https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf

>>2387 >but all [of facebook's] money making infrastructure is all PHP *A typed dialect of PHP called Hack which runs on the HHVM, also made with OCaml.

>>2389 Ignore that part then. I was thinking of the half assed code browser tool they released and that I could never get working properly.

>>2387 https://www.quantamagazine.org/formal-verification-creates-hacker-proof-code-20160920

>>606 >>691 >>2352 >>2375 >>2382 In unrelated news, I saw a whole video lecture about the introduction to Ada being put up on the Volafile room: https://volafile.org/r/kUFzLJ Just saying. First lesson is about all the wrongs and myths that surround Ada. Also Ada is made for huge projects, your average DIY-GitHub coder is simply very unlikely to ever need many of those features and thus probably sees them as useless of even bad. Not that this is true.

>>2440 I think the problem with Ada is licensing. Your choice is, $10,000 compiler or infect your code with the GPL virus.

>>2442 nice bait mate. Now go and read the actual GPL (v2 and v3) and come back when you have understood it. Its the same license used by the GCC, the worlds most used compiler.

>>2447 You're a GPL expert and you never wondered why binaries compiled with GCC are not GPLed too? I think you are the one who needs to do some reading, friend. GCC has a specific exception to avoid passing on the GPL virus to compiled files. https://www.gnu.org/licenses/gcc-exception.html GNAT obviously does not include that exception. http://libre.adacore.com/tools/gnat-gpl-edition/faq/#licensing

>>2449 yeah Im sure you are the very first one to point out this hithero undiscovered fact and everyone else who uses GPLed software just did not understand the dangers they are dealing with. GPL regulates your product and its modifications, not what you create with that product. My Bucket wheel excavator may run exclusively on GPLed software, but that does not put the coal it mines under GPL. Its only if I modify the software that I have to give those changes to those that receive the modified software in sourcecode.

>>2449 I did not know about this exception. What a shame. I had quite a bit of interest in learning Ada and maybe I still will, but I suddenly find myself much less enthusiastic.

>>2450 That's not a fair analogy to how a compiler toolchain turns source into a working executable. This is literally the second paragraph of the link I shared. >When you use GCC to compile a program, GCC may combine portions of certain GCC header files and runtime libraries with the compiled program. The purpose of this Exception is to allow compilation of non-GPL (including proprietary) programs to use, in this way, the header files and runtime libraries covered by this Exception. For what it's worth I'm not trying to disparage the GPL. >>2452 I wasn't trying to put people off of Ada either. I was offering a theory as to why Ada appears "dead" to laymen like >>2375

>>2442 >>2449 >>2455 You got a few things wrong. First of all, as far as I've gathered, the output of a GPL-licensed program is covered by the same license as the input. The exception is when the output contains huge portions of text from the GPL licensed program, and in that case only the parts of the program coming from the text of the program are covered by the GPL. https://www.gnu.org/licenses/gpl-faq.en.html#CanIUseGPLToolsForNF >In such cases, the copied text in the output is covered by the same license that covers it in the source code. Meanwhile, the part of the output which is derived from the program's input inherits the copyright status of the input. A proprietary program can't link against GPL-licensed libraries without violating the GPL, which is why most libraries prefer to use the LGPL, which doesn't have this clause. Linking against GNAT GPL's runtime libraries is what makes a proprietary program violate the GPL. Also, there's two different GPL versions of GNAT: one is AdaCore Libre's, which is not covered by the GCC exception, the other is FSF GNAT (http://www.getadanow.com/), which is covered by that exception.

>>2458 >In such cases, the copied text in the output is covered by the same license that covers it in the source code. Meanwhile, the part of the output which is derived from the program's input inherits the copyright status of the input. Are you sure you read this right? It means the Bison skeleton parser which is copied into your code is GPL, and your own code is whatever license you want. But the combined work still becomes GPL, because one of the components is GPL and that's how the GPL works. This is exactly why the GPL exceptions exist for things like GCC and Bison. >there's two different GPL versions of GNAT Yep, that's my mistake.

>>2473 >the combined work still becomes GPL My bad. That's a bit confusing.

Thanks for pointing out that FSF GNAT exists. I'm glad I was wrong about Ada and licensing.

>>597 Check out Shen.

>>2346 Types express some property about your program. Haskell has typeclasses, which enables you to express properties about types. For instance, if you want to define a mean function, you have to state that the input is a list of stuff that can be divided (which corresponds to the typeclass Fractional), and returns something of the same type, so in Haskell syntax it is Fractional a => [a] -> a With dependent types, you can define types containing terms. For instance, in Coq, you could create the type List nat 5 for the type of lists of natural numbers of size 5. The function tail would have type forall A : Type, forall n : nat, List A (1+n) -> List A n The type proves that tail takes a non-empty list as its input and decrements its size. Going further down the rabbit hole, you could define the type of even and odd numbers (in Coq): Inductive even : nat -> Prop := even0 : even 0 | evenS : forall n : nat, odd n -> even (1+n) with odd : nat -> Prop := oddS : forall n : nat, even n -> odd (1+n). Here, even0 has type (even 0), oddS takes as input a number n and an object of type (even n), therefore oddS 0 even0 has type (odd 1), evenS 1 (oddS 0 even0) has type (even 2), and so on. In other words, you can create an object of type (even n) if, and only if, n is even. Therefore, constructing such an object is a proof n is even. If you want to create a function foo that only takes an even number as its input, give it the type forall n : nat, even n -> ... (n is the first argument of foo, and the proof n is even is the second argument). You can do stuff far more complicated (like proving mathematical stuff), but I believe my post is difficult enough to understand.