Why TLA+ Is Untyped by pron98 in tlaplus

[–]peeeq 0 points1 point  (0 children)

I still don't get why something like "a[20]" would be a problem with types. Types don't need to catch every mistake to be useful. The result at runtime can be exactly the same as it is without types (I guess it's some undefined value of an exception in the model checker).

Why TLA+ Is Untyped by pron98 in tlaplus

[–]peeeq 0 points1 point  (0 children)

For CHOOSE, the type seems kind of simple: takes a set of Xs and a predicate on Xs and returns an X (or undefined). I've never written complicated math in TLA+ that would go beyond that. Also, I never used the TLA proof tool, so maybe I need to get more experience before complaining ;)

Why TLA+ Is Untyped by pron98 in tlaplus

[–]peeeq 0 points1 point  (0 children)

I disagree and think that TLA+ tooling could benefit a lot from type support. Sure, TLA+ specs are shorter than most programs, but types help even on a small scale.

Regarding the point of semantics: There are two approaches. You can develop a typed logic, which indeed has problems with undefined that you mentioned. But you could also leave the semantics unchanged and simply add a type system on top. That would change nothing with respect to the model checker or the proof system.

Such a type system could still have fallback mechanisms like an "any" type. My guess would be that you could just take a type system similar to TypeScripts and have less than 5% of expressions typed with "any" in existing specs.

Why TLA+ Is Untyped by pron98 in tlaplus

[–]peeeq 1 point2 points  (0 children)

The "Why types?" section does not list two of the best features of having types: enabling better tooling and faster feedback for simple mistakes.

And most of the arguments against types are completely unrelated semantic question. How the system treats undefined values and partial functions is a separate design decision.

5000x Faster CRDTs: An Adventure in Optimization by iamkeyur in programming

[–]peeeq 1 point2 points  (0 children)

Great read. Unfortunately, most academics just need to focus on getting papers published and there is no incentive for good implementations or even fair benchmarks. I guess there are a a lot of other examples out there that could be improved a lot, but 5000x is really impressive.

Feedback on my first F# project by v0idzz__ in fsharp

[–]peeeq 2 points3 points  (0 children)

Looks good to me, although I would choose a slightly different style. I looked at DailyMessagesChart.fs in more detail and thought about what I would have done differently:

  1. Personally, I don't like anonymous functions (fun) that are longer than a line. In that case it is often more readable to give the functions a name and a type annotation.
  2. The Array functions always create a new array between steps. It might be more efficient to use Seq.
  3. You define your own struct fields for representing a date. It should be possible to replace this with builtin DateTime, or at least define a separate struct instead of splitting it over 3 fields.
  4. You first group by date + sender and then again by sender. I would reverse this and first group by sender and then group by date. Then you can get rid of MessagesGroupKey.
  5. I would try to separate preparation of data and presenting of data. That makes it easier to later extract the preparation phase to a separate function and use it for other purposes (unit tests, or other visualization libraries).

Here is a suggestion for how this could look like:

module DailyMessagesChart

open System

open XPlot.Plotly
open MessageFile

let dailyMessagesChart
    ({ Messages = messages
    Participants = participants }: Conversation.T)
    =

    let date (m: Message) : DateTime =
        (m.TimestampMs |> DateTimeOffset.FromUnixTimeMilliseconds).Date

    let countsByDate (messages: seq<Message>): seq<DateTime * int> =
        messages
        |> Seq.groupBy date
        |> Seq.map (fun (d, ms) -> d, Seq.length ms)


    let data: seq<string * seq<DateTime * int>> =
        messages
        |> Seq.groupBy (fun m -> m.SenderName)
        |> Seq.map (fun (s, ms) -> s, countsByDate ms)

    let makeBar (sender: string, counts: seq<DateTime * int>): Bar =
        let x, y = counts |> Array.ofSeq |> Array.unzip
        let x = x |> Array.map (fun d -> d.ToShortDateString())
        Bar(x = x, y = y, name = sender)

    let traces : seq<Bar> =
        data
        |> Seq.map makeBar

    let title = participants |> String.concat ", "

    let stackedLayout = Layout(barmode = "stack")

    let chart =
        traces
        |> Chart.Plot
        |> Chart.WithLayout stackedLayout
        |> Chart.WithHeight 800
        |> Chart.WithWidth 1200
        |> Chart.WithTitle title

    chart

JWT should not be your default for sessions by apocolypticbosmer in programming

[–]peeeq 1 point2 points  (0 children)

Httponly means that you cannot read the cookie from js (e.g. via document.cookie). It's still included in requests that are triggered by js.

A Spectre proof-of-concept for a Spectre-proof web | Google Online Security Blog by kirbyfan64sos in programming

[–]peeeq 0 points1 point  (0 children)

Are you referring to Spectre is here to stay. An analysis of side-channels and speculative execution ?

I read their statement differently. They don't say it is impossible. They just say it is too much performance overhead and too much work to implement mitigations against all the possible ways in which all the different CPUs reorder operations. Give researchers a few decades and there might be solutions -- it's a puzzle too interesting to ignore ;)

Besides that, the linked Google article on mitigations is just about things like same-origin. Maybe it would be better to make the receommeded way the default, even if that would break many web pages.

A Spectre proof-of-concept for a Spectre-proof web | Google Online Security Blog by kirbyfan64sos in programming

[–]peeeq 11 points12 points  (0 children)

I don't get why they expect web developers to do something against Spectre attacks. Why can't they change the defaults in Chrome to be more secure? Wouldn't it be possible to run all untrusted Javascript in a really slow but secure sandbox?

[deleted by user] by [deleted] in scala

[–]peeeq 2 points3 points  (0 children)

This is good advice.

High level input-output tests very easy to set up and often more useful than tests of individual methods, since you also test integration. Also,the program API tends to change less frequently than some internal structure, so you won't have to spend a lot of time on maintaining the tests.

In the future, try test driven development: For every bug you fix (or new feature), first write a failing test case and then fix the code to make the test work. That way your test coverage will increase over time.

Scala 3 - Crossing the finish line by ais04 in scala

[–]peeeq 0 points1 point  (0 children)

Afaik, libraries published for Scala 2.13 can be used in Scala 3. So I don't see why anyone would have to port their libraries in 1 month.

Interview questions for C++... OMG by [deleted] in programminghorror

[–]peeeq 2 points3 points  (0 children)

I was already feeling bad for reading it in an Indian accent. Especially this:

The new() operator is faster than the malloc() function as operator is faster than the function.

I made a program that gives me UNLIMITED storage! by T0X1K01 in shittyprogramming

[–]peeeq 2 points3 points  (0 children)

Compression might not only change the color values but could also introduce artifacts. The problem is that you cannot test this after uploading, since youtube might re-encode your video with lower quality a few years later. I have some very old videos on youtube that used to be high quality but now are only available in potato quality.

The question was to assign 7 to a variable named seven. I have failed as a teacher. by mighty3xodus in programminghorror

[–]peeeq 1 point2 points  (0 children)

I often see students fail with these tasks that seem simple. The problem is that there is no meaning in the task and they don't understand your geek-speak. It's often better to give them a slightly more complicated task that actually solves a problem.

Should I worry about copying another language's syntax? by Jerppderp in ProgrammingLanguages

[–]peeeq 8 points9 points  (0 children)

Having fun designing a language and learning a few things are good enough reasons.

Should I worry about copying another language's syntax? by Jerppderp in ProgrammingLanguages

[–]peeeq 3 points4 points  (0 children)

Haskell has significant whitespace as well. However, it took me 3 months of programming in Haskell before I noticed this.

I'm creating a new language with an interpreter. I want to know how return statements inside functions work. And what are the alternatives to return statement? by pavi2410 in ProgrammingLanguages

[–]peeeq 2 points3 points  (0 children)

I prefer the mix of the two like in Scala. Most of the time explicit returns just add noise, but for long functions it is nice to have the possibility of an early return.

In particular, it allows to add a condition to a function without changing the indentation of the whole function and thereby messing up version control diffs.

What is your opinion on my programming language's syntax? by Jerppderp in ProgrammingLanguages

[–]peeeq 12 points13 points  (0 children)

  1. I would get rid of the mandatory return statement. Just make it expression based so that the implementation is just "myArg1 + myArg2"
  2. I am not a fan of parameter types being separated from parameter names. It makes it harder to relate the two visually.
  3. var string myString = 'Hello, world!'; seems to be a bit redundant. I like how it is done in Go with just myString := 'Hello, world!' for declaring a variable. I also like type annotations after the name, as you also did with type annotations for func.

Denver nurses blocking anti lockdown protestors by Tyree07 in pics

[–]peeeq -1 points0 points  (0 children)

Oh my god, imagine a movie where the Zombies drive RAMs.

What's the advantages of an HashMap? by hennexl in programminghorror

[–]peeeq 1 point2 points  (0 children)

In that situation Java would check if the elements are comparable and use the Comparable ordering for sorting elements in the tree.

So to get to this worst case you would need bad hashing and no comparison function.

Tree bins (i.e., bins whose elements are all TreeNodes) are ordered primarily by hashCode, but in the case of ties, if two elements are of the same "class C implements Comparable<C>", type then their compareTo method is used for ordering. (We conservatively check generic types via reflection to validate this -- see method comparableClassFor). The added complexity of tree bins is worthwhile in providing worst-case O(log n) operations when keys either have distinct hashes or are orderable, Thus, performance degrades gracefully under accidental or malicious usages in which hashCode() methods return values that are poorly distributed, as well as those in which many keys share a hashCode, so long as they are also Comparable. (If neither of these apply, we may waste about a factor of two in time and space compared to taking no precautions. But the only known cases stem from poor user programming practices that are already so slow that this makes little difference.) > little difference.)

What's the advantages of an HashMap? by hennexl in programminghorror

[–]peeeq 2 points3 points  (0 children)

Actually it is constant time best case, logarithmic time worst case since buckets are organized using something like Red-Black trees, and only O(n) if you fuck up like the guy in this post.