>Programming Theory Thread, too much normie shit on /g/ edition

>why would I ever do a thing when I could just rely on the work of people smarter than me to do it better
You wouldn't, code monkey

>>57668935

By that logic I should construct my own transistors and discrete electronics too presumably.

Brb harvesting silicate minerals.

>>57669076
You should certainly know how

I don't get it. Is it a rooster thread?

Axiom fu : forall A : Prop, A \/ ~ A.
Check fu.

Axiom iif : forall T (A : Prop), (A -> T) -> (~ A -> T) -> T.
Check iif.
Arguments iif {_} _ _ _.

Axiom iif_true :
  forall T (A : Prop) (ft : A -> T) (ff : ~ A -> T) (H : A),
  iif A ft ff = ft H.
Check iif_true.
Arguments iif_true {_ _} _ _ _.

Axiom iif_false :
  forall T (A : Prop) (ft : A -> T) (ff : ~ A -> T) (H : ~ A),
  iif A ft ff = ff H.
Check iif_false.
Arguments iif_false {_ _} _ _ _.

Definition order_sym := fun T (le : T -> T -> Prop) => forall x, le x x.
Check order_sym.
Arguments order_sym {_} _.

Definition order_total :=
  fun T (le : T -> T -> Prop) => forall x y, le x y \/ le y x.
Check order_total.
Arguments order_total {_} _.

Definition max :=
  fun T (le : T -> T -> Prop) x y =>
    iif (le x y) (fun _ => y) (fun _ => x).
Check max.
Arguments max {_} _ _ _.

Theorem max_is_max :
  forall T (le : T -> T -> Prop) (_ : order_sym le) (_ : order_total le)
    (x y : T),
    let m := max le x y in
    le x m /\ le y m.
intros T le HS HT x y m.
unfold max in m.
case (fu (le x y)).
 intro H.
 assert (m = y).
  apply (iif_true (fun _ : le x y => y) (fun _ : ~ le x y => x)).
  auto.
  rewrite H0.
  auto.
 intro H.
 assert (m = x).
  apply (iif_false (fun _ : le x y => y) (fun _ : ~ le x y => x)).
  auto.
  rewrite H0.
  split.
   apply HS.
   unfold order_total in HT.
   assert (le x y \/ le y x).
    apply HT.
    case H1.
     intro H2.
     exfalso.
     apply H.
     auto.
     auto.
Qed.

you are taking a standard of approach from /g/

while i am not sure what module you are discussing, responses like >>57669187 number in the majority here. Yet the content never ranges beyond porting available libraries to python or from python. It used to be said one does not respond to trolls. That guy responds like his mother. Don't bother with him.

Having said that, what are you talking about? I'll google for now but I'd like to know what you're getting at. It almost sounds like simple integrity checks from before the compiler, to ensure that the system is clean but it could make extension of the system a simpler deal. That there would be more than one person working on any computer is highly possible, that another student would attempt to steal from the others is not as unlikely as we'd all like to think.

oh ok, you're just going over last chapter in every programming book. neeeevermind. im almost certain this is a non issue here because we have access to memory here. at least those of us that dont use the higher level languages.

>>57668901
>Is there tangible benefit to his coding beliefs in 2016
Maybe yes, maybe no.
I think we shouldn't let beliefs guide us into the future.
Or at least we shouldn't blindly follow them.

File: 1476046509837.gif (2MB, 320x240px) Image search: [Google]

2MB, 320x240px

>>57669313
>>57669621

Lookup formal language and formal methods.

Essentially I'm wondering if most programming languages whether they're functional or not use a compiler that is formally designed using these methods that are outlined by Dijkstra

Or are most languages and libraries these days just put together based on practical functionality people need in a language or lib?

There's very sparse information on it outside of Dijkstra's teachings, SICP, and the module I did which was largely theory rather than practical application of the methods. So instead of diving into a lot of reading material I thought I'd ask /g/ for fun.