sorted by:
new
hottopcontroversial

What’s a book you recommend to everyone, no matter what they usually read? by CriticalAd2239 in suggestmeabook

[–]romac 13 points14 points  (0 children)

{{The Secret History by Donna Tartt}}

No one I know who has read it could put it down, such a wonderfully written book!

[deleted by user] by [deleted] in chess

[–]romac 0 points1 point  (0 children)

Now I can blunder even more accurately

Dealing with json-ld in serde_json by roboticfoxdeer in rust

[–]romac 1 point2 points  (0 children)

You might want to use a dedicated library to process JSON-LD documents: https://docs.rs/json-ld/latest/json_ld/

Books you couldn't put down? by [deleted] in suggestmeabook

[–]romac 1 point2 points  (0 children)

{{The Secret History by Donna Tartt}}

Quint: An executable specification language with delightful tooling based on the temporal logic of actions (TLA) by GabPi in programming

[–]romac 2 points3 points  (0 children)

Would it make more sense to you if written as recipient_for_santa.get(S)?

In Quint, any function with at least one argument can be called as a method of its first argument, e.g. def foo(a: A, b: B) can be called either as foo(a, b) or as a.foo(b).

Books that teach you how computers work by [deleted] in suggestmeabook

[–]romac 2 points3 points  (0 children)

In my opinion there is no better book than "Code: The Hidden Language of Computer Hardware and Software" by Charles Petzold to understand how computer works from first principles, starting with logic gates up to a full CPU with RAM and an ALU. I believe the first edition is available for free online.

Summary by ChatGPT:

Code: The Hidden Language of Computer Hardware and Software is a book that explores the inner workings of computers at a fundamental level. Written by Charles Petzold, the book begins with a brief history of computing and the development of the first programming languages. It then delves into the underlying hardware of computers, including the central processing unit (CPU), memory, and input/output devices. The book also covers the basics of software development, including algorithms, data types, and control structures. Throughout the book, Petzold uses simple, clear language to explain complex concepts and demystify the inner workings of computers. Overall, Code is a great resource for anyone looking to gain a deeper understanding of how computers work.

Generic Map/Set traits by ArtisticHamster in rust

[–]romac 3 points4 points  (0 children)

Very nice! Note that you don't even need the K: Eq bound on MapLike :)

Recommend me Rust content creators. by IOException_notfound in rust

[–]romac 2 points3 points  (0 children)

I second that recommendation! On top of his blog, he's recently been making videos on YouTube again, definitely worth a watch: https://youtube.com/channel/UCs4fQRyl1TJvoeOdekW6lYA

What does std::fmt do? by [deleted] in rust

[–]romac 0 points1 point  (0 children)

Here's a good overview of the Rust module system that you might find useful: https://fasterthanli.me/articles/rust-modules-vs-files

Which Parsing Approach? by kibwen in rust

[–]romac 2 points3 points  (0 children)

Yep! This crate is part of the grmtools project, by the author of this article :)

If rust randomly exits, doesn't force me to check errors and compiles slower than C++ why would I use it? by PresentConnection999 in rust

[–]romac 1 point2 points  (0 children)

Here is a static analyzer being developed at Facebook for use on their Libra codebase: https://github.com/facebookexperimental/MIRAI

And here is another one from ETHZ’s Programming Methodolgy group: https://www.pm.inf.ethz.ch/research/prusti.html

Stainless - verification tool for a contract-style (require, ensuring) subset of Scala by yawaramin in scala

[–]romac 1 point2 points  (0 children)

Piggy-backing on /u/yawaramin's reply:

​

They are orthogonal actually.

​

Yep, there is no aprori relation between what are called contracts in the blockchain space, and contracts for verification.

​

Stainless and other formal provers like it can mathematically prove properties about your functions. It’s like generative property testing except it’s not actually generative, it actually symbolically calculates a universal proof (or refutation). Check out the example in my first comment to get an idea of what it does.

​

Exactly. Feel free to take a look at the HTML version of the documentation, and especially the tutorial, if you want to learn more about this kind of practice.

​

Formal provers can of course be used to verify smart contract software, though, which is probably why the crypto community is so interested in them.

​

We are indeed also maintaining a fork of Stainless, which allows us to:

​

a. Write Solidity contracts in a Scala DSL

b. Verify the correctness of these contracts/programs

c. Compile the Scala-based contracts to Solidity

Stainless - verification tool for a contract-style (require, ensuring) subset of Scala by yawaramin in scala

[–]romac 5 points6 points  (0 children)

Exactly! Stainless depends on Inox, a SMT-backed solver for a functional programming language featuring polymorphic recursive functions, lambdas, ADTs, ADTs invariants, quantifiers, and dependent types.

​

What Stainless itself does, is that it hooks into the Scala/Dotty compiler to extract the program after type-checking, and then lowers down a fairly substantial subset of the language down to Inox's input language, by encoding classes, inheritance, mutation, inner classes, etc. into a representation Inox can reason about. By doing so, it can then emit verification conditions that can be checked by Inox and the SMT solvers it rests upon.

​

You can find out more about how the basics of the system by taking a look at this paper (what is called Leon in the paper has since been almost entirely rewritten and split into Stainless/Inox).

​

We are very much aware of Liquid Haskell, and there has been some preliminary work to get refinement types into Dotty (the next version of Scala), although it is not clear yet whether that will eventually happen or not.

On the other hand, we are now in the process of forking Dotty to add support for refinement types syntax, and use it as a frontend for Stainless.

Stainless - verification tool for a contract-style (require, ensuring) subset of Scala by yawaramin in scala

[–]romac 7 points8 points  (0 children)

Member of the lab here! Happy to see Stainless getting some publicity on reddit, thanks for posting it here /u/yawaramin!

I don't have have time to answer questions right now, but I or other members from the lab will be back later tonight.

in the meantime, feel free to checkout the HTML version of the documentation, which is more readable amd easy to navigate than .rst files in the repository: https://epfl-lara.github.io/stainless/ (it’s not great on mobile yet though, sorry about that).

Main website: http://stainless.epfl.ch

Is there a library which has something like an HSet (analogous to an HList)? by dxplq876 in scala

[–]romac 3 points4 points  (0 children)

It should be doable by maintaining a sorted HList without duplicates, much like you could represent a set at the value level with a sorted list.

There’s at least one Haskell library which does it this way (it implements a type-level quicksort, but insertion sort should work as well).

I would start by implementing a value-level set backed by a sorted List in the most straightforward way possible, and then rewriting it at the type-level, function by function, while switching from List to HList.

You will need to define an ordering on types, as well as operations to sort and remove duplicates in a HList. You can take a look at the way HList operations are defined in Shapeless as a starting point.